Implementing Tableaux Calculi Using BDDs: BDDTab System Description

ABSTRACT. Binary Decision Diagrams (BDDs) have been used to decide satisfiability and validity in various non-classical logics by directly implementing the finite property method for these logics. We instead present a method for using Binary Decision Diagrams as an underlying data structure for implementing the tableau method itself. We demonstrate our method by implementing the standard tableau calculi for automated reasoning in propositional modal logics K and S4, along with extensions to the multiple and inverse modalities of ALCI. We evaluate our implementation of such a reasoner using several K and S4 benchmark sets, as well as some ALC and ALCI ontologies. We show, with comparison to FaCT++ and InKreSAT, that it can compete with other state of the art methods of reasoning in propositional modal logic. We also discuss how this technique extends to tableaux for other propositional logics.