Implementing tableau calculi using BDDs: BDDtab system description

Abstract

We present a modification of the DPLL-based approach to decide modal satisfiability where we substitute DPLL by BDDs. 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 modalities of. We evaluate our implementation of such a reasoner using several K and S4 benchmark sets, as well as some ontologies. We show, with comparison to FaCT++, InKreSAT and SAT, 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 tableau for other propositional logics.