Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
From MaRDI portal
Publication:3655207
DOI10.1007/978-3-642-04222-5_18zbMath1193.68225OpenAlexW2144407603MaRDI QIDQ3655207
Stéphane Lescuyer, Sylvain Conchon
Publication date: 7 January 2010
Published in: Frontiers of Combining Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-04222-5_18
Related Items (4)
SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ Efficient, verified checking of propositional proofs ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
Uses Software
Cites Work
- Unnamed Item
- Efficiently checking propositional refutations in HOL theorem provers
- A structure-preserving clause form translation
- Automated proof construction in type theory using resolution
- Automation for interactive proof: first prototype
- Structural Analysis of Narratives with the Coq Proof Assistant
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- Certification of Automated Termination Proofs
- Simplify: a theorem prover for program checking
- Efficient E-Matching for SMT Solvers
- Deciding Equality in the Constructor Theory
- Contraction-free sequent calculi for intuitionistic logic
- Theory and Applications of Satisfiability Testing
- Automated Deduction – CADE-20
- Theorem Proving in Higher Order Logics
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
This page was built for publication: Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
