| dc.contributor.author | Groote, Jan Friso | |
| dc.contributor.author | Tveretina, Olga | |
| dc.date.accessioned | 2014-01-13T16:30:33Z | |
| dc.date.available | 2014-01-13T16:30:33Z | |
| dc.date.issued | 2003 | |
| dc.identifier.citation | Groote , 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.uri | http://hdl.handle.net/2299/12522 | |
| dc.description.abstract | 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 | en |
| dc.language.iso | eng | |
| dc.relation.ispartof | The Journal of Logic and Algebraic Programming | |
| dc.title | Binary decision diagrams for first-order predicate logic | en |
| dc.contributor.institution | School of Physics, Engineering & Computer Science | |
| dc.contributor.institution | Biocomputation Research Group | |
| dc.contributor.institution | Department of Computer Science | |
| dc.description.status | Peer reviewed | |
| rioxxterms.versionofrecord | 10.1016/S1567-8326(03)00039-0 | |
| rioxxterms.type | Journal Article/Review | |
| herts.preservation.rarelyaccessed | true | |
