Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Preprints and Working Papers
  4. Interoperability of Proof Systems with SC-TPTP
 
preprint

Interoperability of Proof Systems with SC-TPTP

Guilloud, Simon  
•
Cailler, Julie
•
Gambhir, Sankalp  
Show more
2025

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.

  • Files
  • Details
  • Version
  • Metrics
Loading...
Thumbnail Image
Name

Interoperability_of_Proof_Systems_with_SC_TPTP_full_version.pdf

Type

Main Document

Version

Not Applicable (or Unknown)

Access type

openaccess

License Condition

CC BY

Size

243.69 KB

Format

Adobe PDF

Checksum (MD5)

e83be70775f1d253e1ac7394e5fee1a9

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés