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

Simon Cruanes simon.cruanes at inria.fr
Wed Jun 28 13:20:34 CEST 2017

Hi Josef,

Sorry, I couldn't access the easychair URL you gave in the previous thread,
and couldn't find a reference on google scholar either. I can't really
compare to the whole state of the art (e.g. I didn't really compare to
IsaPlanner either) but mostly to fully automatic standalone tools that
perform induction in addition to other theories (hence, CVC4, Pirate, …).
The comparison with Leo2/Satallax is not very relevant imho because
using HO unification/enumeration for induction is doomed to fail except
in very simple cases.


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/2b950a59/attachment.sig>

More information about the matryoshka-devel mailing list