@inproceedings{11bb5f2f3da84602a429ecb98dcc5c66,
title = "Implementing modal tableaux using sentential decision diagrams",
abstract = "A Sentential Decision Diagram (SDD) is a novel representation of a boolean function which contains a Binary Decision Diagram (BDD) as a subclass. Previous research suggests that BDDs are effective in implementing tableaux-based automated theorem provers. We investigate whether SDDs can offer improved efficiency when used in the same capacity. Preliminarily, we found that SDDs compile faster than BDDs only on large CNF formulae. In general, we found the BDD-based modal theorem prover still outperforms our SDD-based modal theorem prover. However, the SDD-based approach excels over the BDD-based approach in a select subset of benchmarks that have large sizes and modalities that are less nested or fewer in number.",
author = "Rajeev Gor{\'e} and Li, \{Jason Jingshi\} and Thomas Pagram",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 28th Australasian Joint Conference on Artificial Intelligence, AI 2015 ; Conference date: 30-11-2015 Through 04-12-2015",
year = "2015",
doi = "10.1007/978-3-319-26350-2\_19",
language = "English",
isbn = "9783319263496",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "218--228",
editor = "Jochen Renz and Bernhard Pfahringer",
booktitle = "AI 2015",
address = "Germany",
}