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

Simon Cruanes simon.cruanes at inria.fr
Mon Jun 26 19:44:28 CEST 2017


Le Mon, 26 Jun 2017, Giles Reger a écrit :
> Congratulations on the acceptance.

Thanks!

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

I have clauses with assumptions, same as in AVATAR (i.e. a set of
boolean literals which are not part of the clause itself).
The clauses are really of the form C ← A, and there is no overhead
at the level of superposition.

Inferences inherit the union of the assumptions of the premises (if
compatible); reductions only work if the rewriting clause's assumptions
subsume the rewrited one (so I support branch-aware
demodulation/subsumption/clc).

> 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).
 
I do the same, the SAT solver is used to find UNSAT in the end, and
prune clauses whose assumptions are false at level 0.

The thing I did not implement is to disable clauses whose assumptions
are false in the current model, because it would require a lot of work
on term indices (if I understood correctly the AVATAR paper).

> 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? ;)

Heh, thanks, but that would make the horizontal axis far too wide ;)

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

Indeed, that's a good point. I run my own script for collecting results
but it's not very scalable.

Thanks for all the comments! If you have further questions I'm glad to
discuss with fellow superposition prover authors!

Cheers!

-- 
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/aee14397/attachment-0001.sig>


More information about the matryoshka-devel mailing list