A refined tableau calculus with controlled blocking for the description logic SHOI

Mohammad Khodadadi; Renate A. Schmidt; Dmitry Tishkovsky

doi:10.1007/978-3-642-40537-2_17

A refined tableau calculus with controlled blocking for the description logic SHOI

Mohammad Khodadadi, Renate A. Schmidt, Dmitry Tishkovsky

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

Abstract

The paper presents a tableau calculus with several refinements for reasoning in the description logic SHOI. The calculus uses non-standard rules for dealing with TBox statements. Whereas in existing tableau approaches a fixed rule is used for dealing with TBox statements, we use a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generated with the tableau prover generation prototype MetTel. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox individuals from the application of blocking can be seen as two separate instances of the latter. Experiments show the refinements lead to fewer rule applications and improved performance. © 2013 Springer-Verlag.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Publisher	Springer Nature
Pages	188-202
Number of pages	14
Volume	8123
ISBN (Print)	9783642405365
DOIs	https://doi.org/10.1007/978-3-642-40537-2_17
Publication status	Published - 2013
Event	22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013 - Nancy Duration: 1 Jul 2013 → … http://www.cs.man.ac.uk/ schmidt/publications/KhodadadiSchmidtTishkovsky13a.html

Publication series

Name	Lecture Notes in Computer Science

Conference

Conference	22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013
City	Nancy
Period	1/07/13 → …
Internet address	http://www.cs.man.ac.uk/ schmidt/publications/KhodadadiSchmidtTishkovsky13a.html

Access to Document

10.1007/978-3-642-40537-2_17

Cite this

Khodadadi, M., Schmidt, R. A., & Tishkovsky, D. (2013). A refined tableau calculus with controlled blocking for the description logic SHOI. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci. (Vol. 8123, pp. 188-202). (Lecture Notes in Computer Science). Springer Nature. https://doi.org/10.1007/978-3-642-40537-2_17

Khodadadi, Mohammad ; Schmidt, Renate A. ; Tishkovsky, Dmitry. / A refined tableau calculus with controlled blocking for the description logic SHOI. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 8123 Springer Nature, 2013. pp. 188-202 (Lecture Notes in Computer Science).

@inproceedings{8df0994a93d643a5804165dcdfddc392,

title = "A refined tableau calculus with controlled blocking for the description logic SHOI",

abstract = "The paper presents a tableau calculus with several refinements for reasoning in the description logic SHOI. The calculus uses non-standard rules for dealing with TBox statements. Whereas in existing tableau approaches a fixed rule is used for dealing with TBox statements, we use a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generated with the tableau prover generation prototype MetTel. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox individuals from the application of blocking can be seen as two separate instances of the latter. Experiments show the refinements lead to fewer rule applications and improved performance. {\textcopyright} 2013 Springer-Verlag.",

author = "Mohammad Khodadadi and Schmidt, {Renate A.} and Dmitry Tishkovsky",

year = "2013",

doi = "10.1007/978-3-642-40537-2_17",

language = "English",

isbn = "9783642405365",

volume = "8123",

series = "Lecture Notes in Computer Science",

publisher = "Springer Nature",

pages = "188--202",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

address = "United States",

note = "22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013 ; Conference date: 01-07-2013",

url = "http://www.cs.man.ac.uk/ schmidt/publications/KhodadadiSchmidtTishkovsky13a.html",

}

Khodadadi, M, Schmidt, RA & Tishkovsky, D 2013, A refined tableau calculus with controlled blocking for the description logic SHOI. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 8123, Lecture Notes in Computer Science, Springer Nature, pp. 188-202, 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013, Nancy, 1/07/13. https://doi.org/10.1007/978-3-642-40537-2_17

A refined tableau calculus with controlled blocking for the description logic SHOI. / Khodadadi, Mohammad; Schmidt, Renate A.; Tishkovsky, Dmitry.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 8123 Springer Nature, 2013. p. 188-202 (Lecture Notes in Computer Science).

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

TY - GEN

T1 - A refined tableau calculus with controlled blocking for the description logic SHOI

AU - Khodadadi, Mohammad

AU - Schmidt, Renate A.

AU - Tishkovsky, Dmitry

PY - 2013

Y1 - 2013

N2 - The paper presents a tableau calculus with several refinements for reasoning in the description logic SHOI. The calculus uses non-standard rules for dealing with TBox statements. Whereas in existing tableau approaches a fixed rule is used for dealing with TBox statements, we use a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generated with the tableau prover generation prototype MetTel. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox individuals from the application of blocking can be seen as two separate instances of the latter. Experiments show the refinements lead to fewer rule applications and improved performance. © 2013 Springer-Verlag.

AB - The paper presents a tableau calculus with several refinements for reasoning in the description logic SHOI. The calculus uses non-standard rules for dealing with TBox statements. Whereas in existing tableau approaches a fixed rule is used for dealing with TBox statements, we use a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generated with the tableau prover generation prototype MetTel. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox individuals from the application of blocking can be seen as two separate instances of the latter. Experiments show the refinements lead to fewer rule applications and improved performance. © 2013 Springer-Verlag.

U2 - 10.1007/978-3-642-40537-2_17

DO - 10.1007/978-3-642-40537-2_17

M3 - Conference contribution

SN - 9783642405365

VL - 8123

T3 - Lecture Notes in Computer Science

SP - 188

EP - 202

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

PB - Springer Nature

T2 - 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013

Y2 - 1 July 2013

ER -

Khodadadi M, Schmidt RA, Tishkovsky D. A refined tableau calculus with controlled blocking for the description logic SHOI. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 8123. Springer Nature. 2013. p. 188-202. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-40537-2_17

A refined tableau calculus with controlled blocking for the description logic SHOI

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this