Binary decision diagrams for first-order predicate logic.

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

zbMATH Keywords

Binary decision diagramsAutomatic reasoningFirst-order predicate logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Data structures (68P05)

Related Items (3)

The complexity of reasoning with FODD and GFODD ⋮ Decision-theoretic planning with generalized first-order decision diagrams ⋮ Non-clausal redundancy properties

Cites Work

• 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
• Unnamed Item
• Unnamed Item

This page was built for publication: Binary decision diagrams for first-order predicate logic.