[Matryoshka-devel] [draft] superposition + induction

Mathias Fleury mathias.fleury at mpi-inf.mpg.de
Fri May 5 21:03:48 CEST 2017


Hello Simon,


There is probably no space for it, but some more details about AVATAR
and your implementation in ziperposition would be nice (I know the
general idea behind AVATAR, but not more).


Some typos :

* "Kersani and Peltier modified Prover9 to handle induction [13], but
only for natural numbers; _It_ is unclear how their technique could" ~> it

* "Regular splitting [16] could be used instead of AVATAR_,_ but at the
cost of efficiency.": no comma?

* "contains no variables": no variable? (singular)

* "A Herbrand model is standard if (i) ..., (ii)..., (iii)" ~> (i) ... ;
(ii) ....; (iii) ...?

* "∀P : nat → bool. P(0) ∧ ∀n : nat. P(n) ⇒ P(s(n)) ⇒ ∀n. P(n).": add
parentheses to get ∀P : nat → bool. P(0) ∧ (∀n : nat. P(n) ⇒ P(s(n))) ⇒
∀n. P(n)? (the parentheses are there for the list example)

* 3.1 "superposition relies on a term ordering for orienting equations."
: Superposition (beginning of sentence)


* "6.1 Proving subgoals by Induction" ~> "Subgoal" (capitalisation)

* "This generalization is only performed if the generalized goal still
passes tests successfully." which tests? It would be better to merge
section 6 and 7. Then in the intro of Sect 6. you could refer to the
tests you are doing. Here it seems to be an implicit forward reference.

* "7 Testing conjectures before trying to prove them" capitalisation (at
least Conjectures).


Best,

Mathias


On 04.05.17 12:06, Simon Cruanes wrote:
> Hello everyone,
>
> I am submitting a paper to Frocos '17 about my work on extending a
> Superposition prover (Zipperposition [1]) with structural induction.
> This can be of interest to Matryoshka, since induction is a specific
> form of higher-order reasoning that is critical as soon as datatypes are
> present.  The paper draft can be found at
> https://cedeela.fr/~simon/files/frocos_17_paper.pdf (and will be
> updated). The deadline is tomorrow, but if anyone has comments to make
> even after the deadline…
>
> Best,
>
> [1] https://github.com/c-cube/zipperposition/
>
>
>
> _______________________________________________
> matryoshka-devel mailing list
> matryoshka-devel at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/matryoshka-devel

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20170505/a50520d0/attachment.html>


More information about the matryoshka-devel mailing list