Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Feb 19 17:07
    fachammer synchronize #741
  • Feb 19 17:07

    fachammer on dls-algorithm-for-formula-equations

    improve criterion in documentat… (compare)

  • Feb 18 16:42
    fachammer synchronize #741
  • Feb 18 16:42

    fachammer on dls-algorithm-for-formula-equations

    improve solveFormulaEquation -… remove unnecessary code fix formatting and 4 more (compare)

  • Feb 12 20:20
    Jenkins nightly build failure
  • Feb 12 20:03
    Jenkins nightly build failure
  • Feb 06 13:56
    Travis gapt/gapt (dls-algorithm-for-formula-equations) passed (4032)
  • Feb 06 13:24
    fachammer synchronize #741
  • Feb 06 13:24

    fachammer on dls-algorithm-for-formula-equations

    put advanced simplify into solv… (compare)

  • Feb 05 19:35
    jvierling labeled #742
  • Feb 05 19:29
    jvierling labeled #744
  • Feb 05 19:26
    jvierling assigned #744
  • Feb 05 19:26
    jvierling opened #744
  • Feb 05 19:18
    jvierling commented #741
  • Feb 05 15:43
    jvierling commented #741
  • Feb 05 14:17
    shetzl commented #741
  • Feb 05 14:13
    fachammer commented #741
  • Feb 04 09:42
    Travis gapt/gapt#741 errored (4031)
  • Feb 04 09:41
    Travis gapt/gapt (dls-algorithm-for-formula-equations) errored (4030)
  • Feb 04 09:13
    fachammer synchronize #741
Andreas H. From
@andreasfrom
@gebner roger.
Andreas H. From
@andreasfrom
@shetzl We talked about going to and from an expansion proof to reduce the proof, but I've got one here (for isaplanner/prop_57.smt2) which has around 2000 steps as an LK proof and going back from expansion to LK is taking more than 20 minutes. So that doesn't seem feasible(?)
Andreas H. From
@andreasfrom
Wait, I realised I could cleanStructuralRules it first and then it roundtrips quickly.
Stefan Hetzl
@shetzl
@andreasfrom Yes, cleanStructuralRules should always be cheap.
Jannik Vierling
@jvierling
@gebner How are our substitutions on term and types supposed to behave when one substitutes both term-level variables and type variables simultaneously? Should type variables be substituted before substituting the term variables?
@gebner I am asking this because I ran into a problem with the syntactic unification where the resulting substitution does not unfiy the expressions but I am not sure whether this is a bug in the unification algorithm or in the way the substitution is applied to the term.
@gebner Here is the example
object Example extends scala.App {

  implicit var ctx = Context()

  ctx += hoc"P{?a}: ?a > o"
  ctx += Ti
  ctx += hoc"c:i"

  val t1 = le"P(x:?a)"
  val t2 = le"P(c)"
  val Some( subst ) = syntacticMGU( t1, t2 )
  require( subst( t1 ) == subst( t2 ) )
}
Gabriel Ebner
@gebner
They are supposed to be applied simultaneously. For example you might have a substitution ?a -> list ?b, (x: ?a) -> (nil : list ?b).
Gabriel Ebner
@gebner
Yes, syntacticMGU is buggy here. There are at least two issues with type variables there. Do you want to look into it, or should I just push the fix?
Jannik Vierling
@jvierling
I will look into it.
Jannik Vierling
@jvierling
@gebner Why is hof"⊤" not considered to be an Atom (hof"⊤".asInstanceOf[Atom] fails) ?
Gabriel Ebner
@gebner
Because it's a logical connective.
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.