zipperposition

zipperposition copied to clipboard

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

c-cube

Clause.proof_depth counts ESA-steps as 0

6

`Clause.proof_depth` / `Proof.Step.inferences_perfomed` considers only Inference or Simplifcation steps, but not Esa steps (e.g. Avatar). This might confuse the heuristics using it.

abentkamp

proof checking for avatar

2

The checking of the split rule usually fails.

abentkamp

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

c-cube

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

c-cube

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

c-cube

* [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...

c-cube

* 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) :=...

c-cube

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

c-cube

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

c-cube