[Matryoshka-devel] [draft] superposition + induction

Josef Urban josef.urban at gmail.com
Fri May 5 08:24:23 CEST 2017


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.

Josef




On Thu, May 4, 2017 at 12:06 PM, Simon Cruanes <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…
>
> Best,
>
> [1] https://github.com/c-cube/zipperposition/
>
> --
> Simon Cruanes
>
> http://weusepgp.info/
> key 49AA62B6, fingerprint 949F EB87 8F06 59C6 D7D3  7D8D 4AC0 1D08 49AA
> 62B6
>
> _______________________________________________
> matryoshka-devel mailing list
> matryoshka-devel at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/matryoshka-devel
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20170505/d2784cba/attachment.html>


More information about the matryoshka-devel mailing list