Experimental TPTP to Isar proof translator. Nik Sultana, September 2013
License: CC0 For more info see http://creativecommons.org/publicdomain/zero/1.0/
Description: This implementation was a small experiment to explore how to translate TPTP-encoded proofs produced by the E theorem-prover, into Isar scripts which can be checked using Isabelle/HOL.
The file pceil contains the implementation. It's incomplete and unpolished. If I were to redo this, I would probably implement it in Prolog rather than Python. TPTP problems are encoded in Prolog syntax, are readable using read/1, and therefore can readily be obtained as data within Prolog.
Test data is included in e_proofs.tgz, generated by E 1.8 from problems in TPTP collection version 5.4.0.