Verifying the conversion into CNF in dafny
From MaRDI portal
Publication:2148786
DOI10.1007/978-3-030-88853-4_10OpenAlexW3202267117MaRDI QIDQ2148786FDOQ2148786
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
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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formalization and implementation of modern SAT solvers
- An optimality result for clause form translation
- Formalized proof systems for propositional logic
- versat: A Verified Modern SAT Solver
- The mechanical verification of a DPLL-based satisfiability solver
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Formalization of Abstract State Transition Systems for SAT
- Extracting verified decision procedures: DPLL and resolution
- Title not available (Why is that?)
Uses Software
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)
