BDDs and Automated Deduction

BDDs (binary decision diagrams) are a very succesful tool for handling boolean functions, but one which has not yet attracted the attention of many automated deduction specialists. We give an overview of BDDs from an automated deduction perspective, showing what can be done with them in propositional and rst-order logic, and discuss the parallels to well-known methods like tableaux and resolution.

• Type: Conference
• Year: 1994
• Where: ISMIS
• Authors: Jean Goubault, Joachim Posegga
• Keywords: Artificial Intelligence, Automated Deduction, Binary Decision Diagrams, ISMIS 1994, Succesful Tool