Show simple item record

dc.contributor.authorGroote, Jan Friso
dc.contributor.authorTveretina, Olga
dc.identifier.citationGroote , J F & Tveretina , O 2003 , ' Binary decision diagrams for first-order predicate logic ' , The Journal of Logic and Algebraic Programming , vol. 57 , no. 1-2 , pp. 1-22 .
dc.identifier.otherPURE: 1302674
dc.identifier.otherPURE UUID: e2665a62-279f-48bf-ab70-a1a94c83cde4
dc.identifier.otherScopus: 0042029576
dc.description.abstractBinary 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 examplesen
dc.relation.ispartofThe Journal of Logic and Algebraic Programming
dc.titleBinary decision diagrams for first-order predicate logicen
dc.contributor.institutionDepartment of Computer Science
dc.contributor.institutionSchool of Engineering and Computer Science
dc.description.statusPeer reviewed
rioxxterms.typeJournal Article/Review

Files in this item


There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record