Binary decision diagrams for first-order predicate logic.
From MaRDI portal
Publication:1426055
DOI10.1016/S1567-8326(03)00039-0zbMath1035.03012OpenAlexW1993552393MaRDI 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)
Full work available at URL: https://doi.org/10.1016/s1567-8326(03)00039-0
Logic in computer science (03B70) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Data structures (68P05)
Related Items
The complexity of reasoning with FODD and GFODD ⋮ Decision-theoretic planning with generalized first-order decision diagrams ⋮ Non-clausal redundancy properties
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