Simon Cruanes

(longer term) - [ ] make `'a flex_state.key` json serializable - [ ] have a set of configurations as json files, embedded into the binary by build system magic -...

Summarize progress in proof checking: * [x] update proof generation with renamings (or not), including rewrite steps and demod steps * [x] test this (without checking) on all TPTP; look...

do the De Bruijn switch for rewriting/demod * convert `l=r` into De Bruijn indices (easy) * write matching `env:term db_env -> pattern:term -> term -> term db_env` (where only DB...

an alternative to discount, could be interesting to explore * for forward demod/simp_reflect (all rewrite rules are used, even passive ones) * maybe for forward subsumption, too

- conditional rewriting * [ ] parse `rewrite forall vars. ∧_i a_i => l = r` * [ ] same for clausal rewriting * [ ] handling by *inference* rule...

* [x] inference for acyclicity (not just simplification): given `C ∨ s = t`, look for σ such that `sσ = tσ` is absurd by acyclicity. Then infer `Cσ` from...

* custom induction schema, with a toplevel command + structural induction on datatypes: `inductive (n:nat) := { (zero, {}), (succ(n'), {n'}) }` + induction on sets `inductive (S:set a) :=...

investigate why GEG rational problems are much harder (ordering? missing optim?) → self paramod with, say, transitivity of `

``` ./zipperposition.native --check -t 30 -o none --dot-llproof /tmp/truc.dot examples/regression/gh_7.zf ```

``` ./zipperposition.native --check -t 30 -o none --dot-llproof /tmp/truc.dot examples/GEG022=1_rat.p --debug.llproof 5 ```