LCF-Style Propositional Simplification with BDDs and SAT Solvers

DOI10.1007/978-3-540-71067-7_9MaRDI QIDQ3543649zbMATH OpenOpenAlexFDO

Authors Hasan Amjad

Publication date 4 December 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71067-7_9

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1189106
• Resolution and binary decision diagrams cannot simulate each other polynomially
• scientific article; zbMATH DE number 834569
• Programming Combinations of Deduction and BDD-based Symbolic Calculation
• An improved BDD method for intuitionistic propositional logic: BDDIntKt system description

Cites work

• scientific article; zbMATH DE number 1696436 (Why is no real title available?)
• scientific article; zbMATH DE number 5605058 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• Efficiently checking propositional refutations in HOL theorem provers
• Isabelle. A generic theorem prover
• Programming Combinations of Deduction and BDD-based Symbolic Calculation
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(4)

• Hiding propositional constants in BDDs.
• Simplifying binary propositional theories into connected components twice as fast
• Proving with BDDs and control of information
• An improved BDD method for intuitionistic propositional logic: BDDIntKt system description

Describes a project that uses

Uses Software

• Chaff
• HOL
• PVS
• ML
• MiniSat
• Coq

This page was built for publication: LCF-Style Propositional Simplification with BDDs and SAT Solvers

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