[Matryoshka-devel] [paper] superposition + induction at Frocos 17

Josef Urban josef.urban at gmail.com
Wed Jun 28 12:28:16 CEST 2017


Hi Simon,

On Mon, Jun 26, 2017 at 5:08 PM, Simon Cruanes <simon.cruanes.2007 at m4x.org>
wrote:

> Hello everyone,
>
> I'm very pleased to announce that my paper on Superposition with
> Structural Induction has been accepted at Frocos 2017.
> The current (almost final) version can be found at
> https://cedeela.fr/~simon/files/frocos_17_paper.pdf .
>

Congratulations!


>
> Many thanks to Josef Urban,


So far de nada. In my opinion at least the reference (optimally a
comparison) with TacticToe that I suggested is pretty relevant in the very
first para of the paper:

"Superposition-based theorem provers and SMT (Satisfiability Modulo Theory)
solvers have considerably improved automation in some proof assistants
thanks
to hammers [2, 3]. However, because these proof assistants provide inductive
datatypes, many theorems are out of reach of the automated provers, which
are
not able to perform inductive reasoning. Such theorems include basic
properties
of Peano arithmetic, reasoning about data structures such as lists and
trees,
manipulating syntax trees (which are often represented as a recursive
datatype),
etc."

This weakness of hammers is exactly what TacticToe addresses.

Best,
Josef





> Giles Reger and Mathias Fleury for their
> comments (and of course to Jasmin).
>
> To Giles: I forgot to answer your question about AvatarSimp. The thing
> is, I did not implement the full AVATAR calculus (no freezing/unfreezing
> of clauses based on the model), for lack of time. Therefore the prover
> explores all branches "at the same time". In this setting, AvatarSimp
> allows a closed branch to be effectively pruned (killing clauses in the
> branch).
>
> Also, ground coversets are built by a kind of extension of
> Skolemization: for a variable of type nat, I generate {0, s(n)} where n
> is a fresh Skolem.
>
> --
> Simon Cruanes
>
> http://weusepgp.info/
> key 49AA62B6, fingerprint 949F EB87 8F06 59C6 D7D3  7D8D 4AC0 1D08 49AA
> 62B6
>
> _______________________________________________
> 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/20170628/49f2aa73/attachment.html>


More information about the matryoshka-devel mailing list