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

Simon Cruanes simon.cruanes at inria.fr
Wed Jun 28 08:37:32 CEST 2017

Le Mon, 26 Jun 2017, Giles Reger a écrit :
> For me there is one last question, which is how you introduce the clauses with assumptions. Do you immediately split a clause on creation and replace the clause by its components? Our Playing with AVATAR paper explored different variations of this choice and others. I might play with this idea of keeping all branches live at once, but my immediate feeling is that it would not have a distinct advantage (I guess you’re not claiming it does, just that you didn’t want to implement the branch assertion bit).

Indeed, I don't think it has an advantage, it's just much simpler to
implement. To answer your question, clauses are indeed eagerly split by
a simplification rule (replacing the original clause by several new
clauses), not at creation time.

> You are correct that the disabling requires quite a bit of book-keeping. The most complicated part is handling “conditional reductions” where a clause depending on A,B is reduced by a clause depending on A and then A is retracted but B is not so the reduction must be undone. There is also a very horrible special case within a special case within a special case in the Vampire code that makes Martin Suda angry whenever we discuss it.

I can imagine :-)

I just simplify if branches are compatible (subsumption of assumptions).
Here, again, AvatarSimp is helpful because it can remove assumptions
from potential rewrite rules / subsuming clauses.

> I do feel that some of these things are not clear in the current version of the paper (probably something you don’t want to hear). Although I don’t remember having such thoughts the first time I read it!

It's not really the focus of the paper anyway! But thanks for the


Simon Cruanes

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/20170628/569bdd2b/attachment.sig>

More information about the matryoshka-devel mailing list