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

- Jan 17 17:54fachammer assigned #743
- Jan 17 17:54fachammer commented #743
- Jan 17 15:08shetzl opened #743
- Jan 16 23:10fachammer synchronize #741
- Jan 16 23:10
fachammer on dls-algorithm-for-formula-equations

improve test messages in MoveQu… implement and test removal of r… add removal of redundant quanti… (compare)

- Jan 16 21:52fachammer synchronize #741
- Jan 16 21:52
fachammer on dls-algorithm-for-formula-equations

refactor some code add more unit tests refactor solveFormulaEquation … and 1 more (compare)

- Jan 16 20:18jvierling assigned #742
- Jan 16 20:04jvierling commented #742
- Jan 16 20:03jvierling commented #742
- Jan 16 20:02jvierling opened #742
- Jan 14 15:59
jvierling on develop

update dependencies: ammonite-o… (compare)

- Jan 14 15:38
jvierling on develop

update SBT 1.3.4 -> 1.3.6 (compare)

- Jan 14 13:58jvierling commented #741
- Jan 13 08:09
jvierling on develop

add tests for the declaration o… (compare)

- Jan 07 20:26fachammer synchronize #741
- Jan 07 20:26
fachammer on dls-algorithm-for-formula-equations

optimize imports and remove unn… (compare)

- Jan 06 21:55fachammer commented #741
- Jan 06 21:29fachammer synchronize #741
- Jan 06 21:29
fachammer on dls-algorithm-for-formula-equations

implement dls algorithm preproc… refactor and test preprocessing… weaken input restrictions on so… and 2 more (compare)

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

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?
I can interrupt it though if it's urgent.