Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme

DOI10.1007/978-3-642-04222-5_18MaRDI QIDQ3655207zbMATH OpenOpenAlexFDO

Authors 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

Recommendations

• From proposition to program. Embedding the refinement calculus in Coq
• LF+ in Coq for "fast and loose" reasoning
• A theoretical perspective of coinductive logic programming
• scientific article; zbMATH DE number 2040977
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Coalgebraic logic programming: from Semantics to Implementation
• Co-Logic Programming: Extending Logic Programming with Coinduction
• Formalizing cut elimination of coalgebraic logics in Coq
• Coinductive Logic Programming and Its Applications

Cites work

• scientific article; zbMATH DE number 1303351 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A structure-preserving clause form translation
• Automated Deduction – CADE-20
• Automated proof construction in type theory using resolution
• Automation for interactive proof: first prototype
• Certification of Automated Termination Proofs
• Contraction-free sequent calculi for intuitionistic logic
• Deciding Equality in the Constructor Theory
• Efficient E-Matching for SMT Solvers
• Efficiently checking propositional refutations in HOL theorem provers
• Simplify: a theorem prover for program checking
• Structural analysis of narratives with the Coq proof assistant
• Theorem Proving in Higher Order Logics
• Theory and Applications of Satisfiability Testing
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

Cited in

(5)

• Functional encryption for inner product with full function privacy
• SAT solving for termination proofs with recursive path orders and dependency pairs
• LF+ in Coq for "fast and loose" reasoning
• Efficient, verified checking of propositional proofs
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

Describes a project that uses

Uses Software

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

This page was built for publication: Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3655207)