Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme

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

Mathematics Subject Classification ID

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

• Coq
• MiniSat
• z3
• SIMPLIFY
• Zenon
• Chaff

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