Using the TPTP Language for Representing Derivations in Tableau and Connection Calculi
Jens Otten, Geoff Sutcliffe · EPiC series in computing · 2018
The TPTP language, developed within the framework of the TPTP library, allows the representation of problems and solutions in first-order and higher-order logic. Whereas the writing of solutions in resolution calculi is well documented and used, an appropriate representation of solutions in tableau or connection calculi using the TPTP syntax has not yet been specified. This paper describes how the TPTP language can be used to represent derivations and solutions in standard tableau, sequent and connection calculi for classical first-order logic.