\textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format

DOI10.1007/978-3-031-30823-9_19MaRDI QIDQ6535368zbMATH OpenFDO

Authors Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa

Publication date 13 December 2023

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Recommendations

• Rocket-Fast Proof Checking for SMT Solvers
• SMT proof checking using a logical framework
• Efficient, verified checking of propositional proofs
• Fast LCF-Style Proof Reconstruction for Z3
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

Cites work

• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• A framework for defining logics
• A mathematical introduction to logic.
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Abstract state machines, Alloy, B, TLA, VDM, and Z. 6th international conference, ABZ 2018, Southampton, UK, June 5--8, 2018. Proceedings
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• Extending Sledgehammer with SMT solvers
• Fast Decision Procedures Based on Congruence Closure
• Flexible proof production in an industrial-strength SMT solver
• On solving quantified bit-vector constraints using invertibility conditions
• OpenSMT2: an SMT solver for multi-core and cloud computing
• Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
• Reliable reconstruction of fine-grained proofs in a proof assistant
• SMT proof checking using a logical framework
• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Satisfiability modulo theories
• Scalable fine-grained proofs for formula processing
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• versat: A Verified Modern SAT Solver

This page was built for publication: \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format

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