\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 QIDQ6535368
Hanna Lachnitt, Bruno Andreotti, Haniel Barbosa
Publication date: 13 December 2023
Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)
Cites Work
- Abstract state machines, Alloy, B, TLA, VDM, and Z. 6th international conference, ABZ 2018, Southampton, UK, June 5--8, 2018. Proceedings
- A verified SAT solver framework with learn, forget, restart, and incrementality
- On solving quantified bit-vector constraints using invertibility conditions
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Flexible proof production in an industrial-strength SMT solver
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Extending Sledgehammer with SMT solvers
- SMT proof checking using a logical framework
- A mathematical introduction to logic.
- OpenSMT2: An SMT Solver for Multi-core and Cloud Computing
- versat: A Verified Modern SAT Solver
- 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
- Solving SAT and SAT Modulo Theories
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- Fast Decision Procedures Based on Congruence Closure
- A framework for defining logics
- Scalable fine-grained proofs for formula processing
This page was built for publication: \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
