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

Giles Reger giles.reger at manchester.ac.uk
Mon Jun 26 18:18:23 CEST 2017


Hi Simon,

Congratulations on the acceptance.

Thanks for the reply. I am not sure I fully understand what you have implemented. Without the freezing/unfreezing it sounds more like splitting without backtracking [1,2] depending on how you introduce the assertions… but I now cannot see a discussion of this in the current version. Indeed it is not clear how superposition is lifted to clauses with assertions, or are the assertions treated as propositional symbols? If the labels are separated how do reductions deal with them? If they are treated as propositional symbols then they are likely to get in the way of reductions.

Of course AVATAR was directly inspired by splitting without backtracking but separating the assertions from the first-order reasoning AVATAR is the way that the assertion-reasoning is performed exclusively by a SAT solver and how the labels do not get in the way of first-order reasoning (which they do in splitting without backtracking).

My inference is that you only use the SAT solver in one direction i.e. to collect constraints not to assert a model, am I right?

By the way, would you like a version of Vampire to allow you to add it to Figure 5? ;)

I can also recommend using StarExec for such experiments as Geoff maintains a set of solvers that you can borrow for your own experiments without the hassle of installing them yourself.

Cheers, Giles

[1] http://dl.acm.org/citation.cfm?id=1642174
[2] https://link.springer.com/chapter/10.1007/978-3-642-38574-2_33

On 26 Jun 2017, at 16:08, Simon Cruanes <simon.cruanes.2007 at m4x.org<mailto: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 .

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
_______________________________________________
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/20170626/b2b3629e/attachment.html>


More information about the matryoshka-devel mailing list