Modular SMT Proofs for Fast Reflexive Checking Inside Coq
From MaRDI portal
Publication:3100210
DOI10.1007/978-3-642-25379-9_13zbMath1350.68224MaRDI QIDQ3100210
Frédéric Besson, David Pichardie, Pierre Cornilleau
Publication date: 22 November 2011
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_13
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Efficiently checking propositional refutations in HOL theorem provers
- A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
- A compiled implementation of strong reduction
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- Simplify: a theorem prover for program checking
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- Simplification by Cooperating Decision Procedures
- Formal certification of a compiler back-end or
- Automated Deduction – CADE-20
- Theorem Proving in Higher Order Logics
- Term Rewriting and Applications
- Extending Coq with Imperative Features and Its Application to SAT Verification
- Fast LCF-Style Proof Reconstruction for Z3
- Tools and Algorithms for the Construction and Analysis of Systems
