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

- 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
- Mar 09 13:21jvierling synchronize #741
- Mar 09 13:21
jvierling on dls-algorithm-for-formula-equations

move DLS algorithm to subpackag… import DLS algorithm in GAPT pr… (compare)

- Mar 09 07:39Travis gapt/gapt#741 broken (4059)
- Mar 09 07:34jvierling synchronize #741
- Mar 09 07:34
jvierling on dls-algorithm-for-formula-equations

move preprocessing related meth… move partial witness extraction… refactor witness combination and 5 more (compare)

- Mar 06 16:53jvierling synchronize #741
- Mar 06 16:53
jvierling on dls-algorithm-for-formula-equations

refactor preprocessing phase of… Merge branch 'dls-algorithm-for… move simplify and related metho… (compare)

- Mar 06 14:58jvierling closed #746
- Mar 06 14:58jvierling commented #746
- Mar 06 14:15fachammer commented #746
- Mar 06 14:14fachammer synchronize #741
- Mar 06 14:14
fachammer on dls-algorithm-for-formula-equations

consider second order variables… (compare)

- Mar 06 10:18jvierling synchronize #741
- Mar 06 10:18
jvierling on dls-algorithm-for-formula-equations

make solveFormulaEquations work… move crossProduct to gapt.utils clean up crossProduct and 5 more (compare)

- Mar 06 07:29fachammer commented #741

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

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.

You can integrate clausification into the saturation loop using this inference: https://github.com/gapt/gapt/blob/2c46e4e159b34fd24969bba15c39b6f02ddbb1a7/core/src/main/scala/gapt/provers/escargot/inferences.scala#L179

But for first-order problems, clausification happens before the main loop is even started.

@gebner At https://github.com/gapt/gapt/blob/2c46e4e159b34fd24969bba15c39b6f02ddbb1a7/core/src/main/scala/gapt/provers/escargot/inferences.scala#L454 what are the positions

`pos2`

supposed to represent?
The first line of the function arguments describes the equation (

`i1`

th formula in clause `c1`

, we want to rewrite `t_`

to `s_`

), the second line describes the other clause that we want to rewrite (`i2`

th 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_)`

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