\textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
From MaRDI portal
Publication:6535368
DOI10.1007/978-3-031-30823-9_19zbMATH Open1543.68395MaRDI QIDQ6535368FDOQ6535368
Authors: Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa 
Publication date: 13 December 2023
Recommendations
Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)
Cites Work
- A mathematical introduction to logic.
- A framework for defining logics
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Extending Sledgehammer with SMT solvers
- SMT proof checking using a logical framework
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- Satisfiability modulo theories
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- Fast Decision Procedures Based on Congruence Closure
- versat: A Verified Modern SAT Solver
- Abstract state machines, Alloy, B, TLA, VDM, and Z. 6th international conference, ABZ 2018, Southampton, UK, June 5--8, 2018. Proceedings
- Reliable reconstruction of fine-grained proofs in a proof assistant
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Scalable fine-grained proofs for formula processing
- OpenSMT2: an SMT solver for multi-core and cloud computing
- A verified SAT solver framework with learn, forget, restart, and incrementality
- On solving quantified bit-vector constraints using invertibility conditions
- Flexible proof production in an industrial-strength SMT 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)
