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

Simon Cruanes simon.cruanes.2007 at m4x.org
Mon Jun 26 17:08:13 CEST 2017


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 .

Many thanks to Josef Urban, 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20170626/4c5fbcdf/attachment.sig>


More information about the matryoshka-devel mailing list