Optimal and cut-free tableaux for propositional dynamic logic with converse

Rajeev Goré; Florian Widmann

doi:10.1007/978-3-642-14203-1_20

Optimal and cut-free tableaux for propositional dynamic logic with converse

Rajeev Goré^*, Florian Widmann

^*Corresponding author for this work

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

20 Citations (Scopus)

Abstract

We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the use of analytic cut. Our main contribution is a sound method to combine our previous optimal method for tracking least fix-points in PDL with our previous optimal method for handling converse in the description logic ALCI. The extension is non-trivial as the two methods cannot be combined naively. We give sufficient details to enable an implementation by others. Our OCaml implementation seems to be the first theorem prover for CPDL.

Original language	English
Title of host publication	Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings
Pages	225-239
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-14203-1_20
Publication status	Published - 2010
Event	5th International Joint Conference on Automated Reasoning, IJCAR 2010 - Edinburgh, United Kingdom Duration: 16 Jul 2010 → 19 Jul 2010

Publication series

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

Conference

Conference	5th International Joint Conference on Automated Reasoning, IJCAR 2010
Country/Territory	United Kingdom
City	Edinburgh
Period	16/07/10 → 19/07/10

Access to Document

10.1007/978-3-642-14203-1_20

Cite this

Goré, R., & Widmann, F. (2010). Optimal and cut-free tableaux for propositional dynamic logic with converse. In Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings (pp. 225-239). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6173 LNAI). https://doi.org/10.1007/978-3-642-14203-1_20

@inproceedings{6fe2ac1726464caa81adb156417b0749,

title = "Optimal and cut-free tableaux for propositional dynamic logic with converse",

abstract = "We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the use of analytic cut. Our main contribution is a sound method to combine our previous optimal method for tracking least fix-points in PDL with our previous optimal method for handling converse in the description logic ALCI. The extension is non-trivial as the two methods cannot be combined naively. We give sufficient details to enable an implementation by others. Our OCaml implementation seems to be the first theorem prover for CPDL.",

author = "Rajeev Gor{\'e} and Florian Widmann",

year = "2010",

doi = "10.1007/978-3-642-14203-1\_20",

language = "English",

isbn = "3642142028",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "225--239",

booktitle = "Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings",

note = "5th International Joint Conference on Automated Reasoning, IJCAR 2010 ; Conference date: 16-07-2010 Through 19-07-2010",

}

Goré, R & Widmann, F 2010, Optimal and cut-free tableaux for propositional dynamic logic with converse. in Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6173 LNAI, pp. 225-239, 5th International Joint Conference on Automated Reasoning, IJCAR 2010, Edinburgh, United Kingdom, 16/07/10. https://doi.org/10.1007/978-3-642-14203-1_20

Optimal and cut-free tableaux for propositional dynamic logic with converse. / Goré, Rajeev; Widmann, Florian.
Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings. 2010. p. 225-239 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6173 LNAI).

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

TY - GEN

T1 - Optimal and cut-free tableaux for propositional dynamic logic with converse

AU - Goré, Rajeev

AU - Widmann, Florian

PY - 2010

Y1 - 2010

N2 - We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the use of analytic cut. Our main contribution is a sound method to combine our previous optimal method for tracking least fix-points in PDL with our previous optimal method for handling converse in the description logic ALCI. The extension is non-trivial as the two methods cannot be combined naively. We give sufficient details to enable an implementation by others. Our OCaml implementation seems to be the first theorem prover for CPDL.

AB - We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the use of analytic cut. Our main contribution is a sound method to combine our previous optimal method for tracking least fix-points in PDL with our previous optimal method for handling converse in the description logic ALCI. The extension is non-trivial as the two methods cannot be combined naively. We give sufficient details to enable an implementation by others. Our OCaml implementation seems to be the first theorem prover for CPDL.

UR - https://www.scopus.com/pages/publications/77955233683

U2 - 10.1007/978-3-642-14203-1_20

DO - 10.1007/978-3-642-14203-1_20

M3 - Conference Paper

SN - 3642142028

SN - 9783642142024

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

SP - 225

EP - 239

BT - Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings

T2 - 5th International Joint Conference on Automated Reasoning, IJCAR 2010

Y2 - 16 July 2010 through 19 July 2010

ER -

Goré R, Widmann F. Optimal and cut-free tableaux for propositional dynamic logic with converse. In Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings. 2010. p. 225-239. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-14203-1_20

Optimal and cut-free tableaux for propositional dynamic logic with converse

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this