[Matryoshka-devel] CASC travel prize in THF division

Blanchette, J.C. j.c.blanchette at vu.nl
Tue Jun 12 11:49:12 CEST 2018

Hi Stephan,

> It’s a fake prize, anyways! It comes with money, bit it does not come
> with the time to actually do the travelling ;-). I still have not
> gone to Munich....

Couldn't you work on the train?

> P.S.: Why does Isabelle not print proofs?

When I developed the TPTP-based command-line interface, building on Nik Sultana's TPTP parser, my goal was to have something simple that works at the competition. But back then, there was no requirement on proofs, so not only I didn't have Isabelle produce TSTP proofs, but furthermore I let Sledgehammer invoke some provers in "oracle" mode, whereby their proofs are not reconstructed.

For most provers, reconstruction would be possible and succeed with a high success rate (> 95%), but there's one method that yields no proof at all, namely the Nitpick model finder on finite HO problems (problems involving only the Boolean type $o and the function arrow >). It was never designed as a prover, but I found that it gives Isabelle an edge on Satallax et al. on a handful of problems.

In the longer run, my goal is to address these issues, with the Matryoshka provers and the Nunchaku model finder. But it will surely take years before we're there...



More information about the matryoshka-devel mailing list