[Matryoshka-devel] [draft] superposition + induction

Simon Cruanes simon.cruanes at inria.fr
Thu May 4 12:06:02 CEST 2017

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
-------------- 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/20170504/ff9e744a/attachment.sig>

More information about the matryoshka-devel mailing list