Show simple item record

dc.contributor.authorGroote, Jan Friso
dc.contributor.authorTveretina, Olga
dc.date.accessioned2014-01-13T16:30:33Z
dc.date.available2014-01-13T16:30:33Z
dc.date.issued2003
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 . https://doi.org/10.1016/S1567-8326(03)00039-0
dc.identifier.otherPURE: 1302674
dc.identifier.otherPURE UUID: e2665a62-279f-48bf-ab70-a1a94c83cde4
dc.identifier.otherScopus: 0042029576
dc.identifier.urihttp://hdl.handle.net/2299/12522
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.language.isoeng
dc.relation.ispartofThe Journal of Logic and Algebraic Programming
dc.titleBinary decision diagrams for first-order predicate logicen
dc.contributor.institutionSchool of Computer Science
dc.contributor.institutionScience & Technology Research Institute
dc.description.statusPeer reviewed
dc.relation.schoolSchool of Computer Science
dcterms.dateAccepted2003
rioxxterms.versionofrecordhttps://doi.org/10.1016/S1567-8326(03)00039-0
rioxxterms.typeJournal Article/Review
herts.preservation.rarelyaccessedtrue


Files in this item

FilesSizeFormatView

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record