Verifying the conversion into CNF in dafny

DOI10.1007/978-3-030-88853-4_10MaRDI QIDQ2148786zbMATH OpenOpenAlexFDO

Authors Viorel Iordache, Ştefan Ciobâcă

Publication date 24 June 2022

Full work available at URL https://doi.org/10.1007/978-3-030-88853-4_10

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• On conversions from CNF to ANF
• Using ÆtnaNova to formally prove that the Davis-Putnam satisfiability test is correct
• An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL
• CNF and DNF considered harmful for computing prime implicants/implicates

Cites work

• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 3325539 (Why is no real title available?)
• scientific article; zbMATH DE number 7699437 (Why is no real title available?)
• A verified SAT solver framework with learn, forget, restart, and incrementality
• An optimality result for clause form translation
• Extracting verified decision procedures: DPLL and resolution
• Formalization and implementation of modern SAT solvers
• Formalization of Abstract State Transition Systems for SAT
• Formalized proof systems for propositional logic
• The mechanical verification of a DPLL-based satisfiability solver
• versat: A Verified Modern SAT Solver

Describes a project that uses

Uses Software

• Archive Formal Proofs
• GNATprove
• versat
• VCC
• Why3
• Dafny
• Coq

This page was built for publication: Verifying the conversion into CNF in dafny

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