[Matryoshka-devel] [paper] superposition + induction at Frocos 17
simon.cruanes at inria.fr
Wed Jun 28 13:20:34 CEST 2017
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.
key 49AA62B6, fingerprint 949F EB87 8F06 59C6 D7D3 7D8D 4AC0 1D08 49AA 62B6
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: not available
More information about the matryoshka-devel