@inproceedings{f78cdcde94814511958b9a133ecbee22,
title = "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.",
author = "Rajeev Gor{\'e} and Kerry Olesen and Jimmy Thomson",
year = "2014",
doi = "10.1007/978-3-319-08587-6\_25",
language = "English",
isbn = "9783319085869",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "337--343",
booktitle = "Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings",
address = "Germany",
note = "7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 ; Conference date: 19-07-2014 Through 22-07-2014",
}