Defining the meaning of TPTP formatted proofs
Roberto Blanco, Tomer Libal, Dale Armin Miller · EPiC series in computing · 2018
The TPTP library is one of the leading problem libraries in the automated theorem proving community. Along the years, support was added for problems beyond those in first-order clausal form. Another addition was the augmentation of the language to support proofs outputted from theorem provers and the maintenance of a proof library, called TSTP. In this paper we propose another augmentation of the language for the support of the semantics of the inference rules used in these proofs.