[Matryoshka-devel] [draft] superposition + induction

Giles Reger giles.reger at manchester.ac.uk
Fri May 5 08:58:06 CEST 2017

Hi Simon,

I like this. I have a few comments that may or may not be useful - as I only read it quickly I may have misunderstood some points. And some comments may not be very useful on the day of submission!

The middle of page 7 is quite dense. If space allows, perhaps slightly more explanation of what you are actually doing here would improve readability (at least for me). The examples are, of course, helpful, but it is the intuition about the structure of the approach and relation to the more obvious induction schema that took me a little bit to unpick.

For Remark 1, I am not sure about the need for AvatarSimp rules, to me it would seem that if a is propagated at level 0 then AVATAR just stops making decisions on it, and we gain the same effect (although perhaps it affects simplification). However, the original paper is not exactly precise about such things, and the remark does add something so I am not suggesting removing it! (btw, http://easychair.org/publications/paper/AVATAR_Modulo_Theories gives a calculus for AVATAR)

There were a few areas where it is clear that your solver needs to make a choice but it is not clear exactly how it makes this choice. There is a lot of example-driven discussion, which is really nice to read, but I was left a little unsure how I could implement all of the ideas in Vampire as suggested ;)

For example, the instantiation in 4.2 requires ground coversets, where do they come from?

In 6.1 you say "A clause C containing at least one inductive skolem can be negated…”, does this mean that your implementation will do this for all such C (the same for the following line). Or do you employ any further heuristics on how to select such clauses.

In 7, do you mean that you start a separate saturation loop, or do you emulate this within the main loop?

Btw, you won’t have time now but for experiments like the one in Figure 5, Geoff maintains the provers you mention (as well as Vampire) on StarExec along with the latest TPTP and it is very easy to just run the same experiment there and compare against other solvers for free!

Finally, I understood all of the AVATAR comments as I am familiar with AVATAR, but I am not sure that the general reader would understand the true import of this case splitting i.e. that one case is selected at a time and explored separately - which is enforced by the exclusive disjunction on page 7.

Cheers, Giles

On 5 May 2017, at 07:24, Josef Urban <Josef.Urban at gmail.com<mailto:Josef.Urban at gmail.com>> wrote:

Hi Simon,

thanks, it's a very good research topic.

More related work:

- I wonder how this compares to systems like TacticToe (http://easychair.org/publications/paper/TacticToe_Learning_to_Reason_with_HOL4_Tactics) on inductive problems from ITP libraries. A similar system is developed for Isabelle: http://aitp-conference.org/2017/slides/yutaka_aitp2017.pdf

- higher-order ATPs like Satallax in principle also solve problems with induction.


On Thu, May 4, 2017 at 12:06 PM, Simon Cruanes <simon.cruanes at inria.fr<mailto:simon.cruanes at inria.fr>> wrote:
Hello everyone,

I am submitting a paper to Frocos '17 about my work on extending a
Superposition prover (Zipperposition [1]) with structural induction.
This can be of interest to Matryoshka, since induction is a specific
form of higher-order reasoning that is critical as soon as datatypes are
present.  The paper draft can be found at
https://cedeela.fr/~simon/files/frocos_17_paper.pdf (and will be
updated). The deadline is tomorrow, but if anyone has comments to make
even after the deadline…


[1] https://github.com/c-cube/zipperposition/

Simon Cruanes

key 49AA62B6, fingerprint 949F EB87 8F06 59C6 D7D3  7D8D 4AC0 1D08 49AA 62B6

matryoshka-devel mailing list
matryoshka-devel at lists.gforge.inria.fr<mailto:matryoshka-devel at lists.gforge.inria.fr>

matryoshka-devel mailing list
matryoshka-devel at lists.gforge.inria.fr<mailto:matryoshka-devel at lists.gforge.inria.fr>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20170505/a271a550/attachment-0001.html>

More information about the matryoshka-devel mailing list