Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Mar 03 07:57

    jvierling on leancopparser

    rearrange formula parser (compare)

  • Mar 02 18:07

    jvierling on develop

    remove some unused variables (compare)

  • Mar 01 16:46

    jvierling on leancopparser

    fix export for variables starti… Merge branch 'leancopparser' in… fix comment and 1 more (compare)

  • Mar 01 11:20

    jvierling on develop

    fix comment (compare)

  • Mar 01 10:48
    Jenkins develop failure
  • Mar 01 10:44

    jvierling on develop

    use quantifier block instead of… make leancop parser a bit more … improve formatting and 3 more (compare)

  • Mar 01 10:42

    jvierling on leancopparser

    (compare)

  • Mar 01 10:17

    Ermine516 on leancopparser

    Current stage of development Instance file production is now… Updating Dummy Prover and 10 more (compare)

  • Mar 01 10:10
    Travis gapt/gapt (InstanceConstructionAndDummyProver) broken (4138)
  • Mar 01 10:05

    Ermine516 on InstanceConstructionAndDummyProver

    Bump version to 2.16-SNAPSHOT update iProver output parser disable superposition and non e… and 32 more (compare)

  • Mar 01 00:25
    Jenkins nightly build failure
  • Feb 28 19:01

    jvierling on leancopparser

    improve formatting refactor definitional clausal f… refactor expansion proof constr… (compare)

  • Feb 27 19:08

    jvierling on leancopparser

    make leancop parser a bit more … (compare)

  • Feb 27 15:17

    Ermine516 on InstanceConstructionAndDummyProver

    Some unimportant changes (compare)

  • Feb 27 15:13

    Ermine516 on InstanceConstructionAndDummyProver

    minor changes (compare)

  • Feb 27 13:25
    Jenkins nightly build failure
  • Feb 27 12:55
    Jenkins develop failure
  • Feb 27 12:51

    jvierling on develop

    fix export for variables starti… (compare)

  • Feb 27 11:50
    Travis gapt/gapt@d49a228 (leancopparser) passed (4132)
  • Feb 27 11:16

    jvierling on leancopparser

    use quantifier block instead of… (compare)

Gabriel Ebner
@gebner
Treating true/false as atoms can easily lead to bugs: e.g. gapt/gapt#309 If they are not atoms, it's clear that you need to treat them specially.
Jannik Vierling
@jvierling
Ok thanks.
Jannik Vierling
@jvierling
@gebner How does Escargot deal with and ? Does it avoid to generate these connectives? The problem is that at some point a ends up as a component by splitting but it is apparently not meant to be there.
Gabriel Ebner
@gebner
There should not be any ⊤ or ⊥ left after clausification.
But for first-order problems, clausification happens before the main loop is even started.
Jannik Vierling
@jvierling
I am running Escargot on a tip problem which uses formulas on term level, this introduces ⊤ after clausificiation.
Gabriel Ebner
@gebner
Goodbye completeness, I think. But yeah, I'd just add the clausification inference rule and see what happens.
Jannik Vierling
@jvierling
I'll try to integrate the clausification ( simplification of ⊤ and ⊥) with the saturation loop.
Jannik Vierling
@jvierling
I think these positions are the positions of some subterms of the forms_ in c_2.conclusion(i2). Is that correct?
Gabriel Ebner
@gebner
The first line of the function arguments describes the equation (i1th formula in clause c1, we want to rewrite t_ to s_), the second line describes the other clause that we want to rewrite (i2th formula in clause c2). pos2 are positions in c2.conclusion(i2) that can be unified with t_ (the left-hand side of the equation, if leftToRight is true). https://github.com/gapt/gapt/blob/2c46e4e159b34fd24969bba15c39b6f02ddbb1a7/core/src/main/scala/gapt/provers/escargot/inferences.scala#L460 These positions are then replaced by the right-hand side of the equation, i.e., mgu(s_).
Andreas H. From
@andreasfrom
If I run ./viper.sh --analytic isaplanner/prop_17.smt2 it fails with a gapt.proofs.gaptic.TacticFailureException and the message goal is not subsumed by provided proof:. This also affects at least prop_25, 33 and 34 and is the same for the spind mode. Is this is a known thing?
Jannik Vierling
@jvierling
@andreasfrom Thanks for reporting this. I fixed the problem.
Andreas H. From
@andreasfrom
@shetzl Generalization only makes a difference for one file: prod/prop_15. Removing testing means going from 127 solved to 97.
Gabriel Ebner
@gebner
@andreasfrom What are your plans for clogic89 for the next few days? Can I have it?
Andreas H. From
@andreasfrom
@gebner Yes, knock yourself out.
Andreas H. From
@andreasfrom
@gebner Please let me know when you're done with it :)
Gabriel Ebner
@gebner
According to parallel, the ETA is 8 d + 8 h + 50 min. But I think it will be finished a bit sooner, since I expect the jobs at the beginning to take significantly longer than the rest.
I can interrupt it though if it's urgent.
Andreas H. From
@andreasfrom
No hurry, thanks for the ETA.
Gabriel Ebner
@gebner
@andreasfrom It's finished now. Do you want to run something now or should I start something else?
Andreas H. From
@andreasfrom
I'll run something over night real quick.
Andreas H. From
@andreasfrom
@gebner clogic89 is yours again. Thanks.
Andreas H. From
@andreasfrom
What's the clogic89 status? I would like to run some (hopefully final) benchmarks this week.
Gabriel Ebner
@gebner
It's yours. Tell me when you're finished.
Andreas H. From
@andreasfrom
Thanks. I expect around 24 hours. I'll let you know.
Andreas H. From
@andreasfrom
@gebner I'm finished.
Gabriel Ebner
@gebner
Jannik Vierling
@jvierling
Thanks
Gabriel Ebner
@gebner
fyi using clogic89 today
Jannik Vierling
@jvierling
@gebner Why does ./gapt.sh somescript execute everything that extends Script?
Gabriel Ebner
@gebner
@jvierling Because someone asked me to make ./gapt.sh poset/cutintro.scala work. 🤷 (I think the request was for another script file though..)
Jannik Vierling
@jvierling
@gebner Thanks for the reply. I was a bit surprised to see ./gapt.sh somescript start to evaluate all Script objects.
Jannik Vierling
@jvierling
@quicquid I have rebased your commit 287a164656bc60a806d63e3b12f2bf06cc3749c4 on develop. I also did two commits on your 'push_version_2.13.3' branch (these are now on develop as well) before I noticed that the branch is not a feature branch. You can now remove these commits from your branch. Please delete the 'push_version_2.13.3' branch when you are done with it.
Martin
@quicquid
@jvierling hi jannik, thank you very much! just a question: i had to rewrite infix binary operators to explicit form, i.e. update + (x,y) to update.+(x,y) because apparently, scala 3 will get extensionality and won't be able to decide if it should curry the function or not. It's a bit ugly because it still works for infix unary functions but i guess renaming + is also not much more readable.
Jannik Vierling
@jvierling
@quicquid As far as I see there are at least two solutions to this problem: 1) We let the method + (of the class PreSubstitution) accept Pairs or 2) As you have already pointed out we could rename +. The first option has the disadvantage that it becomes more difficult to speak about the "two" parameters of the function i.e. it obfuscates the method signature. The second option has the disadvantage that it makes the code less concise but on the other hand we could choose a name that conveys more semantic information (such as e.g. 'extend' or 'extendBy'). Such method names are quite readable but do not fit in well with the functional style.
Martin
@quicquid
I agree - since the code is already merged, the pull request doesn't need to be adapted anymore. We might just keep it in mind if it comes up at some point.
Martin
@quicquid
i'm not sure who exactly to ask, but do you remember why you didn't put proofs into a context? i'm just doing some cleanup and would like to get rid of the ExtendedProofDB
Jannik Vierling
@jvierling
To be honest I don't know much about the LLK format. As far as I see, the only purpose of ExtendedProofDatabase is to associate proofs with formulas (and to keep track of some definitions and axioms). Technically it should be possible to move all this into the Context (as a facet), but I think that the proof database is somewhat linked to the LLK format and therefore I would not like to integrate it into the context whose responsibility is to keep track of the logical language and the background theories.
Martin
@quicquid
I introduced LLK when I started my thesis ages ago and it has been superseded by Gaptic since. One of my aims is to get rid of it (which should make maintenance of GAPT easier) and transfer all code needing it to Gaptic. I had some time this summer to rewrite my old proofs and they've become much shorter in terms of inferences ( https://derivation.org/nTape2old.png vs. https://derivation.org/nTape2new.png ) but they also take less effort to describe (800 lines vs 250 lines) :-) I'd still like to preserve the old formalization for comparison and documuntation, but we have the JSON format for that now.
I'm currently adapting the cut-elimination code to the new proofs (the hol2fol encoding that just erases types doesn't work with the new version) and would like to make a pull request once everything works again, if that's ok :)
Jannik Vierling
@jvierling
Yes of course that's OK. Just make sure to branch off from develop. Migrating all the LLK related stuff to Gaptic sounds like a good idea since the latter is much more documented.
Martin
@quicquid
Sure - As maintainer, feel free to make requests to adjust the patch to the project :) I could have taken care of the rebasing etc as well :)
Ermine516
@Ermine516
Hello all, currently developing an experiment using Viper and realized I need to recompile GAPT to debug
I forgot the procedure. it has been too long.
Can someone send me the steps to recompile. Thanks!
Jannik Vierling
@jvierling
You can use sbt clean followed by sbt compile to recompile everything.