Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Apr 08 11:54
    Travis gapt/gapt (develop) fixed (4074)
  • Apr 08 11:20

    jvierling on develop

    update to scala 2.13.1 (compare)

  • Apr 08 11:12
    Travis gapt/gapt (develop) broken (4073)
  • Apr 08 11:09

    jvierling on develop

    update SBT 1.3.6 -> 1.3.9 update sbt plugins update dependencies (compare)

  • Apr 08 08:20

    jvierling on develop

    bump version number to 2.15.1 fix 2.15 release notes add 2.15.1 release notes and 1 more (compare)

  • Apr 08 08:19
    Travis gapt/gapt (v2.15.1) errored (4071)
  • Apr 08 08:11
    Jenkins gapt failure
  • Apr 08 08:07

    jvierling on v2.15.1

    (compare)

  • Apr 08 08:07

    jvierling on master

    bump version number to 2.15.1 fix 2.15 release notes add 2.15.1 release notes and 1 more (compare)

  • Apr 01 14:04
    quicquid commented #740
  • Mar 30 18:32
    Jenkins nightly build failure
  • Mar 30 18:04
    Jenkins develop failure
  • Mar 30 17:56
    jvierling commented #740
  • Mar 30 17:53

    jvierling on develop

    update iProver output parser disable superposition and non e… (compare)

  • Mar 30 13:35

    jvierling on prooftransform

    (compare)

  • Mar 30 13:35

    jvierling on structural_induction

    (compare)

  • Mar 30 13:34

    jvierling on tip-smt-parser

    (compare)

  • Mar 30 13:34

    jvierling on release-2.15

    (compare)

  • Mar 30 13:33

    jvierling on dls-algorithm-for-formula-equations

    (compare)

  • Mar 30 09:14
    Travis gapt/gapt (v2.15) passed (4067)
Jannik Vierling
@jvierling
Our Tip importer not very sophisticated so for the moment we will have to deal with certain cases where the error messages are not very comprehensible. However when using 'fixupAndLoad' many more problems can be parsed.
Andreas H. From
@andreasfrom
Okay, I will use that one instead. Thanks!
Jannik Vierling
@jvierling
If you need the importer to support any features that it can't currently handle, then let me know so that I can implement them.
Andreas H. From
@andreasfrom
Adding axioms one at a time and doing a couple of loops in between improves spind a bit. I think testing axioms before adding them might potentially help a lot. (timeout also increased from 30s to 45s)
mode
analytic_independent    17
analytic_sequential     40
spind                   15
treegrammar              7
Stefan Hetzl
@shetzl
@andreasfrom This looks better!
I could very well image that testing is quite useful.
It may also be worthwhile to have a closer look at the difference between independent and sequential induction axioms, maybe spind can somehow emulate the use of the sequential induction axioms
Jannik Vierling
@jvierling
@andreasfrom I have updated the tip tool on the server. The problems should now parse.
Andreas H. From
@andreasfrom
@shetzl Yes, I will look at what @jannikvierling sent me and take a closer look.
@jannikvierling Great, thank you!
Gabriel Ebner
@gebner
@andreasfrom Are you planning on doing any experiments on clogic89 between now and Thursday?
Gabriel Ebner
@gebner
@andreasfrom I'm running some experiments on clogic89 today. Please don't run anything else at the moment.
Gabriel Ebner
@gebner
@andreasfrom Also using clogic89 today.
Ermine516
@Ermine516
@jannikvierling Sorry I was delayed in message you, Vacation :)
I am back now
Is there a gapt meeting today?
Gabriel Ebner
@gebner
No, happy easter!
Ermine516
@Ermine516
If so I can bring it with me and we can discuss
:D, ah yes that is why I was on vacation, right.
Happy easter to you too
see you next week then
Gabriel Ebner
@gebner
Next week is labor day.
Ermine516
@Ermine516
ok, I should look at my calendar then
Andreas H. From
@andreasfrom
@gebner Sorry, didn't see your message. I only ran some stuff yesterday. If you need it today and tomorrow please let me know.
Gabriel Ebner
@gebner
Nah, everything's already done now. Also the deadline got extended by two weeks, so I'm no longer in such a hurry either.
Stefan Hetzl
@shetzl
@Ermine516 The next regular gapt meeting is scheduled for May 15.
Andreas H. From
@andreasfrom

I have a question about importing TIP problems. The file tip2015/list_return_2.smt2 looks like this:

; List monad laws
(declare-datatypes (a)
  ((list (nil) (cons (head a) (tail (list a))))))
(define-fun (par (a) (return ((x a)) (list a) (cons x (_ nil a)))))
(define-fun-rec
  (par (a)
    (++
       ((x (list a)) (y (list a))) (list a)
       (match x
         (case nil y)
         (case (cons z xs) (cons z (++ xs y)))))))
(define-fun-rec
  (par (a b)
    (>>=
       ((x (list a)) (y (=> a (list b)))) (list b)
       (match x
         (case nil (_ nil b))
         (case (cons z xs) (++ (@ y z) (>>= xs y)))))))
(prove
  (par (a)
    (forall ((xs (list a)))
      (= (>>= xs (lambda ((x a)) (return x))) xs))))

and after fixupAndLoad becomes:

∀x0 ∀x1 head(cons(x0, x1)) = x0,
∀x0 ∀x1 tail(cons(x0, x1)) = x1,
∀x return(x) = cons(x, nil),
lam2 = lam,
∀y ++(nil, y) = y,
∀y ∀z ∀xs ++(cons(z, xs), y) = cons(z, ++(xs, y)),
∀y >>=(nil, y) = nil,
∀y ∀z ∀xs >>=(cons(z, xs), y) = ++(apply1(y, z), >>=(xs, y)),
∀y0 ∀y1 nil != cons(y0, y1),
∀x apply1(lam, x) = return(x)
⊢
∀xs >>=(xs, lam2) = xs
So the apply1 must be introduced by the tip tool, but it does not show up in TipProblem.functions which I am using to generate reduction rules for testing.
Jannik Vierling
@jvierling
The symbol apply1 is stored in TipProblem.uninterpretedConsts, because it has no definition.
Andreas H. From
@andreasfrom
Why doesn't ∀x apply1(lam, x) = return(x) constitute a definition?
Jannik Vierling
@jvierling
Actually by definition I meant a definition in terms of define-fun or define-fun-rec or define-funs-rec. Actually the tip tool adds the definition that you gave as an assertion with a :definition keyword, but currently the tip importer does not inspect these keywords.
Andreas H. From
@andreasfrom
Oh right. Okay, thank you.
Jannik Vierling
@jvierling
Next week when I am back i'll try to spend some time to improve the tip importer.
Andreas H. From
@andreasfrom
It's not urgent for my purposes.
Andreas H. From
@andreasfrom

Here's an update:

mode
analytic_independent    43
analytic_sequential     75
spind                   34
treegrammar             16

All the problems solved by the analytic independent mode are affected by the tip importer thing mentioned above which makes my testing of conjectures less efficient or straight up breaks it. Three of them are solved if I just disable testing.

Spind is currently a little slower in total on the problems they have in common:

spind                118,666ms
analytic_independent 93,527ms
Gabriel Ebner
@gebner
@andreasfrom I'm going to use clogic89 over the weekend again.
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.