Ground truth: checking \textsc{Vampire} proofs via satisfiability modulo theories

DOI10.1007/978-3-031-99984-0_8MaRDI QIDQ6869957zbMATH OpenFDO

Authors Michael G. Rawson, Andrei Voronkov, Johannes Schoisswohl, Anja Petković Komel

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_8

zbMATH Keywords

automated theorem provingSMTverified proofs

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

• \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• ALASCA: reasoning in quantified linear arithmetic
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• AVATAR: The Architecture for First-Order Theorem Provers
• Contradiction separation based dynamic multi-clause synergized automated deduction
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• scientific article; zbMATH DE number 7699423 (Why is no real title available?)
• IeanCOP: lean connection-based theorem proving
• Induction for SMT solvers
• Induction in saturation
• IPASIR-up: user propagators for CDCL
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Resolution theorem proving
• Satisfiability modulo theories
• Superposition with first-class booleans and inprocessing clausification
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• The TPTP typed first-order form with arithmetic
• Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
• 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
• Translating higher-order clauses to first-order clauses
• Unification with abstraction and theory instantiation in saturation-based reasoning
• VIRAS: conflict-driven quantifier elimination for integer-real arithmetic
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

This page was built for publication: Ground truth: checking \textsc{Vampire} proofs via satisfiability modulo theories

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