Binary decision diagrams for first-order predicate logic
Groote, Jan Friso and Tveretina, Olga
(2003)
Binary decision diagrams for first-order predicate logic.
pp. 1-22.
Binary decision diagrams (BDDs) are known to be a very efficient technique to handle propositional formulas. We present an extension of BDDs such that they can be used for predicate logic. We define BDDs similar to Bryant [IEEE Trans. Comp. C-35 (1986) 677–691], but with the difference that we allow predicates as labels instead of proposition symbols. We present a sound and complete proof search method for first-order predicate logic based on BDDs which we apply to a number of examples
Item Type | Article |
---|---|
Date Deposited | 14 Nov 2024 11:19 |
Last Modified | 14 Nov 2024 11:19 |