Hiding propositional constants in BDDs.

DOI10.1007/BF00121264zbMATH Open1425.68088OpenAlexW3016442180MaRDI QIDQ960509FDOQ960509

Authors: Jan Friso Groote 

Publication date: 21 December 2008

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00121264

Recommendations

• Binary decision diagrams for first-order predicate logic.
• Extended Resolution Proofs for Conjoining BDDs
• BDDs -- design, analysis, complexity, and applications.
• LCF-Style Propositional Simplification with BDDs and SAT Solvers
• scientific article; zbMATH DE number 1863167

zbMATH Keywords

binary decision diagrampropositional logicsatifiability

Mathematics Subject Classification ID

Data structures (68P05) Classical propositional logic (03B05) Logic in computer science (03B70)

Cites Work

• Graph-Based Algorithms for Boolean Function Manipulation

Cited In (2)

• Stålmarck's algorithm as a HOL derived rule
• The Complexity of Propositional Proofs

This page was built for publication: Hiding propositional constants in BDDs.

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