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

Josef Urban josef.urban at gmail.com
Wed Jun 28 14:29:24 CEST 2017

Oops, they changed the URL. Now at
https://easychair.org/publications/paper/340355 . Josef

On Wed, Jun 28, 2017 at 1:20 PM, Simon Cruanes <simon.cruanes at inria.fr>

> 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.
> Best,
> --
> Simon Cruanes
> http://weusepgp.info/
> key 49AA62B6, fingerprint 949F EB87 8F06 59C6 D7D3  7D8D 4AC0 1D08 49AA
> 62B6
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20170628/dba40351/attachment-0001.html>

More information about the matryoshka-devel mailing list