Binary decision diagrams for first-order predicate logic.
From MaRDI portal
Publication:1426055
DOI10.1016/S1567-8326(03)00039-0zbMath1035.03012MaRDI QIDQ1426055
Jan Friso Groote, Olga Tveretina
Publication date: 14 March 2004
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
03B70: Logic in computer science
03B10: Classical first-order logic
03B35: Mechanization of proofs and logical operations
68P05: Data structures
Cites Work
- Unnamed Item
- Unnamed Item
- Termination of rewriting
- Errata to ``75 problems for testing automatic theorem provers
- Symbolic model checking: \(10^{20}\) states and beyond
- Linear unification
- Resolution and binary decision diagrams cannot simulate each other polynomially
- Graph-Based Algorithms for Boolean Function Manipulation
- Hard examples for resolution
- An Efficient Unification Algorithm
- Automated Deduction with Shannon Graphs