- Join over
**1.5M+ people** - Join over
**100K+ communities** - Free
**without limits** - Create
**your own community**

- Apr 01 14:04quicquid commented #740
- Mar 30 18:32Jenkins nightly build failure
- Mar 30 18:04Jenkins develop failure
- Mar 30 17:56jvierling 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

- Mar 30 13:35
jvierling on structural_induction

- Mar 30 13:34
jvierling on tip-smt-parser

- Mar 30 13:34
jvierling on release-2.15

- Mar 30 13:33
jvierling on dls-algorithm-for-formula-equations

- Mar 30 08:57
jvierling on develop

update release notes. Release 2.15. Bump version to 2.16-SNAPSHOT (compare)

- Mar 30 08:44
jvierling on v2.15

- Mar 30 08:26
jvierling on release-2.15

Release 2.15. (compare)

- Mar 30 08:22Travis gapt/gapt@fc1dcd3 (release-2.15) passed (4064)
- Mar 30 07:50
jvierling on release-2.15

update release notes. (compare)

- Mar 23 11:10
shetzl on develop

remove unnecessary includes (compare)

- Mar 09 14:03
jvierling on develop

implement simplified DLS algori… refactor solveFormulaEquation return substitution from solveF… and 73 more (compare)

- Mar 09 14:03jvierling closed #741

@jannikvierling Yes, sorry I should have said I did try that, but it didn't seem to make much of a difference, giving me errors directly from the tip tool instead. Here is an example where

`fixupAndLoad`

just gives a different error (because of this, I think):```
scala> val problem = TipSmtImporter.fixupAndLoad("benchmarks/isaplanner/prop_02.smt2")
java.util.NoSuchElementException: None.get
```

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
```

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

@jannikvierling Great, thank you!

I am back now

Is there a gapt meeting today?

:D, ah yes that is why I was on vacation, right.

Happy easter to you too

see you next week then

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.
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
```

@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(?)

@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 ) )
}
```