Binary decision diagrams for first-order predicate logic

Jan Friso Groote, Olga Tveretina

Research output: Contribution to journalArticlepeer-review

20 Citations (Scopus)


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
Original languageEnglish
Pages (from-to)1-22
JournalThe Journal of Logic and Algebraic Programming
Issue number1-2
Publication statusPublished - 2003


Dive into the research topics of 'Binary decision diagrams for first-order predicate logic'. Together they form a unique fingerprint.

Cite this