Interoperability of proof systems with SC-TPTP

DOI10.1007/978-3-031-99984-0_18MaRDI QIDQ6869945zbMATH OpenFDO

Authors Simon Guilloud, Julie Cailler, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat, Viktor Kuncak

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_18

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
• A generic deskolemization strategy
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• Certified dominance and symmetry breaking for combinatorial optimisation
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Efficient certified RAT verification
• Fast Decision Procedures Based on Congruence Closure
• Fast LCF-Style Proof Reconstruction for Z3
• Faster, higher, stronger: E 2.3
• Hammer for Coq: automation for dependent type theory
• Hammering towards QED
• HOL Light: An Overview
• scientific article; zbMATH DE number 7699423 (Why is no real title available?)
• IeanCOP: lean connection-based theorem proving
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• LISA -- a modern proof system
• On the complexity of proof deskolemization
• Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
• Reliable reconstruction of fine-grained proofs in a proof assistant
• Semantics and proof theory of the epsilon calculus
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Term Rewriting and Applications
• The Lean theorem prover (system description)
• The logic languages of the TPTP world
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee
• TPTP, TSTP, CASC, etc.
• Translating HOL-Light proofs to Coq

This page was built for publication: Interoperability of proof systems with SC-TPTP

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6869945)