Interoperability of Proof Systems with SC-TPTP
We introduce SC-TPTP, an extension of the TPTP derivation format that encompasses sequent formalism, enabling seamless proof exchange between interactive theorem provers and first-order automated theorem provers. We provide a way to represent non-deductive steps-Skolemization, clausification, and Tseitin normal form-as deductive steps within the format. Building upon the existing support in the Lisa proof assistant and the Goéland theorem prover, SC-TPTP ecosystem is further enhanced with proof output interfaces for Egg and Prover9, as well as proof reconstruction support for HOL Light, Lean, and Rocq.
Interoperability_of_Proof_Systems_with_SC_TPTP_full_version.pdf
Main Document
http://purl.org/coar/version/c_be7fb7dd8ff6fe43
openaccess
CC BY
243.69 KB
Adobe PDF
e83be70775f1d253e1ac7394e5fee1a9