Sound global state caching for ALC with inverse roles

Rajeev Goré; Florian Widmann

doi:10.1007/978-3-642-02716-1_16

Sound global state caching for ALC with inverse roles

Rajeev Goré^*, Florian Widmann

^*Corresponding author for this work

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

24 Citations (Scopus)

Abstract

We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability with respect to a TBox in the logic ALCI using global state caching. Global state caching guarantees optimality and termination without dynamic blocking, but in the presence of inverse roles, the proofs of soundness and completeness become significantly harder. We have implemented the algorithm in OCaml, and our initial comparison with FaCT++ indicates that it is a promising method for checking satisfiability with respect to a TBox.

Original language	English
Title of host publication	Automated Reasoning with Analytic Tableaux and Related Methods - 18th International Conference, TABLEAUX 2009, Proceedings
Pages	205-219
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-02716-1_16
Publication status	Published - 2009
Event	18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009 - Oslo, Norway Duration: 6 Jul 2009 → 10 Jul 2009

Publication series

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

Conference

Conference	18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009
Country/Territory	Norway
City	Oslo
Period	6/07/09 → 10/07/09

Access to Document

10.1007/978-3-642-02716-1_16

Cite this

Goré, R., & Widmann, F. (2009). Sound global state caching for ALC with inverse roles. In Automated Reasoning with Analytic Tableaux and Related Methods - 18th International Conference, TABLEAUX 2009, Proceedings (pp. 205-219). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5607 LNAI). https://doi.org/10.1007/978-3-642-02716-1_16

@inproceedings{dd4d20a2509b4502bf2641f465b06962,

title = "Sound global state caching for ALC with inverse roles",

abstract = "We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability with respect to a TBox in the logic ALCI using global state caching. Global state caching guarantees optimality and termination without dynamic blocking, but in the presence of inverse roles, the proofs of soundness and completeness become significantly harder. We have implemented the algorithm in OCaml, and our initial comparison with FaCT++ indicates that it is a promising method for checking satisfiability with respect to a TBox.",

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

year = "2009",

doi = "10.1007/978-3-642-02716-1_16",

language = "English",

isbn = "3642027156",

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

pages = "205--219",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 18th International Conference, TABLEAUX 2009, Proceedings",

note = "18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009 ; Conference date: 06-07-2009 Through 10-07-2009",

}

Goré, R & Widmann, F 2009, Sound global state caching for ALC with inverse roles. in Automated Reasoning with Analytic Tableaux and Related Methods - 18th International Conference, TABLEAUX 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5607 LNAI, pp. 205-219, 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009, Oslo, Norway, 6/07/09. https://doi.org/10.1007/978-3-642-02716-1_16

Sound global state caching for ALC with inverse roles. / Goré, Rajeev; Widmann, Florian.
Automated Reasoning with Analytic Tableaux and Related Methods - 18th International Conference, TABLEAUX 2009, Proceedings. 2009. p. 205-219 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5607 LNAI).

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

TY - GEN

T1 - Sound global state caching for ALC with inverse roles

AU - Goré, Rajeev

AU - Widmann, Florian

PY - 2009

Y1 - 2009

N2 - We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability with respect to a TBox in the logic ALCI using global state caching. Global state caching guarantees optimality and termination without dynamic blocking, but in the presence of inverse roles, the proofs of soundness and completeness become significantly harder. We have implemented the algorithm in OCaml, and our initial comparison with FaCT++ indicates that it is a promising method for checking satisfiability with respect to a TBox.

AB - We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability with respect to a TBox in the logic ALCI using global state caching. Global state caching guarantees optimality and termination without dynamic blocking, but in the presence of inverse roles, the proofs of soundness and completeness become significantly harder. We have implemented the algorithm in OCaml, and our initial comparison with FaCT++ indicates that it is a promising method for checking satisfiability with respect to a TBox.

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

U2 - 10.1007/978-3-642-02716-1_16

DO - 10.1007/978-3-642-02716-1_16

M3 - Conference contribution

SN - 3642027156

SN - 9783642027154

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

SP - 205

EP - 219

BT - Automated Reasoning with Analytic Tableaux and Related Methods - 18th International Conference, TABLEAUX 2009, Proceedings

T2 - 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009

Y2 - 6 July 2009 through 10 July 2009

ER -

Goré R, Widmann F. Sound global state caching for ALC with inverse roles. In Automated Reasoning with Analytic Tableaux and Related Methods - 18th International Conference, TABLEAUX 2009, Proceedings. 2009. p. 205-219. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-02716-1_16

Sound global state caching for ALC with inverse roles

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this