Implementing tableau calculi using BDDs: BDDtab system description

Rajeev Goré; Kerry Olesen; Jimmy Thomson

doi:10.1007/978-3-319-08587-6_25

Implementing tableau calculi using BDDs: BDDtab system description

Rajeev Goré, Kerry Olesen, Jimmy Thomson

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

9 Citations (Scopus)

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.

Original language	English
Title of host publication	Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
Publisher	Springer Verlag
Pages	337-343
Number of pages	7
ISBN (Print)	9783319085869
DOIs	https://doi.org/10.1007/978-3-319-08587-6_25
Publication status	Published - 2014
Event	7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria Duration: 19 Jul 2014 → 22 Jul 2014

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8562 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
Country/Territory	Austria
City	Vienna
Period	19/07/14 → 22/07/14

Access to Document

10.1007/978-3-319-08587-6_25

Cite this

Goré, R., Olesen, K., & Thomson, J. (2014). Implementing tableau calculi using BDDs: BDDtab system description. In Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings (pp. 337-343). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8562 LNAI). Springer Verlag. https://doi.org/10.1007/978-3-319-08587-6_25

Goré, Rajeev ; Olesen, Kerry ; Thomson, Jimmy. / Implementing tableau calculi using BDDs : BDDtab system description. Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. pp. 337-343 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@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",

}

Goré, R, Olesen, K & Thomson, J 2014, Implementing tableau calculi using BDDs: BDDtab system description. in Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8562 LNAI, Springer Verlag, pp. 337-343, 7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 19/07/14. https://doi.org/10.1007/978-3-319-08587-6_25

Implementing tableau calculi using BDDs: BDDtab system description. / Goré, Rajeev; Olesen, Kerry; Thomson, Jimmy.
Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, 2014. p. 337-343 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8562 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Implementing tableau calculi using BDDs

T2 - 7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014

AU - Goré, Rajeev

AU - Olesen, Kerry

AU - Thomson, Jimmy

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84958544119&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-08587-6_25

DO - 10.1007/978-3-319-08587-6_25

M3 - Conference contribution

SN - 9783319085869

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 337

EP - 343

BT - Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings

PB - Springer Verlag

Y2 - 19 July 2014 through 22 July 2014

ER -

Goré R, Olesen K, Thomson J. Implementing tableau calculi using BDDs: BDDtab system description. In Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag. 2014. p. 337-343. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-08587-6_25

Implementing tableau calculi using BDDs: BDDtab system description

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this