[Matryoshka-devel] Some HOL Problems which might be in the range of Matryoshka

Martin Riener riener at logic.at
Mon Jul 17 15:46:53 CEST 2017

Hi everyone,

I wrote a short summary of the background for some THF problems I
generated in the last months. The idea was to work in a fragment close
to first-order logic (with FO equality) such that I could benefit from
the SAT/FOL back-ends of HO ATPs. This did not work out as well as I
expected, but in particular finite approximations of a function might be
in the range of a future Matryoshka.

I'm not sure if I can get all the problems into the TPTP, but you can
find them here, if you'd like to have a look (and maybe I just
overlooked prover X which magically solves something ):


cheers, Martin

More information about the matryoshka-devel mailing list