A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI

M Khodadadi; R A Schmidt; D Tishkovsky; Thomas Eiter; Birte Glimm; Yevgeny Kazakov; Markus Krötzsch

A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI

M Khodadadi, R A Schmidt, D Tishkovsky, Thomas Eiter (Editor), Birte Glimm (Editor), Yevgeny Kazakov (Editor), Markus Krötzsch (Editor)

Research output: Chapter in Book/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, the tableau calculus uses a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generatedwith 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.

Original language	English
Title of host publication	Proceedings of the 26th International Workshop on Description Logics (DL-2013)
Editors	Thomas Eiter, Birte Glimm, Yevgeny Kazakov, Markus Krötzsch
Publisher	RWTH Aachen University
Pages	724-734
Number of pages	11
Volume	Vol-1014
Publication status	Published - 2013

Publication series

Name	CEUR Workshop Proceedings

Access to Document

Cite this

Khodadadi, M., Schmidt, R. A., Tishkovsky, D., Eiter, T. (Ed.), Glimm, B. (Ed.), Kazakov, Y. (Ed.), & Krötzsch, M. (Ed.) (2013). A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI. In T. Eiter, B. Glimm, Y. Kazakov, & M. Krötzsch (Eds.), Proceedings of the 26th International Workshop on Description Logics (DL-2013) (Vol. Vol-1014, pp. 724-734). (CEUR Workshop Proceedings). RWTH Aachen University. http://www.cs.man.ac.uk/~schmidt/publications/KhodadadiSchmidtTishkovsky13b.html\url{http://ceur-ws.org/Vol-1014/paper_28.pdf}

Khodadadi, M ; Schmidt, R A ; Tishkovsky, D et al. / A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI. Proceedings of the 26th International Workshop on Description Logics (DL-2013). editor / Thomas Eiter ; Birte Glimm ; Yevgeny Kazakov ; Markus Krötzsch. Vol. Vol-1014 RWTH Aachen University, 2013. pp. 724-734 (CEUR Workshop Proceedings).

@inproceedings{615f1d188cf7477db3117a53744572c5,

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, the tableau calculus uses a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generatedwith 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.",

author = "M Khodadadi and Schmidt, {R A} and D Tishkovsky and Thomas Eiter and Birte Glimm and Yevgeny Kazakov and Markus Kr{\"o}tzsch",

year = "2013",

language = "English",

volume = "Vol-1014",

series = "CEUR Workshop Proceedings",

publisher = "RWTH Aachen University",

pages = "724--734",

editor = "Thomas Eiter and Birte Glimm and Yevgeny Kazakov and Markus Kr{\"o}tzsch",

booktitle = "Proceedings of the 26th International Workshop on Description Logics (DL-2013)",

address = "Germany",

}

Khodadadi, M, Schmidt, RA, Tishkovsky, D, Eiter, T (ed.), Glimm, B (ed.), Kazakov, Y (ed.) & Krötzsch, M (ed.) 2013, A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI. in T Eiter, B Glimm, Y Kazakov & M Krötzsch (eds), Proceedings of the 26th International Workshop on Description Logics (DL-2013). vol. Vol-1014, CEUR Workshop Proceedings, RWTH Aachen University, pp. 724-734. <http://www.cs.man.ac.uk/~schmidt/publications/KhodadadiSchmidtTishkovsky13b.html\url{http://ceur-ws.org/Vol-1014/paper_28.pdf}>

A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI. / Khodadadi, M; Schmidt, R A; Tishkovsky, D et al.
Proceedings of the 26th International Workshop on Description Logics (DL-2013). ed. / Thomas Eiter; Birte Glimm; Yevgeny Kazakov; Markus Krötzsch. Vol. Vol-1014 RWTH Aachen University, 2013. p. 724-734 (CEUR Workshop Proceedings).

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

TY - GEN

T1 - A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI

AU - Khodadadi, M

AU - Schmidt, R A

AU - Tishkovsky, D

A2 - Eiter, Thomas

A2 - Glimm, Birte

A2 - Kazakov, Yevgeny

A2 - Krötzsch, Markus

A2 - Eiter, Thomas

A2 - Glimm, Birte

A2 - Kazakov, Yevgeny

A2 - Krötzsch, Markus

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, the tableau calculus uses a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generatedwith 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.

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, the tableau calculus uses a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generatedwith 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.

M3 - Conference contribution

VL - Vol-1014

T3 - CEUR Workshop Proceedings

SP - 724

EP - 734

BT - Proceedings of the 26th International Workshop on Description Logics (DL-2013)

PB - RWTH Aachen University

ER -

Khodadadi M, Schmidt RA, Tishkovsky D, Eiter T, (ed.), Glimm B, (ed.), Kazakov Y, (ed.) et al. A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI. In Eiter T, Glimm B, Kazakov Y, Krötzsch M, editors, Proceedings of the 26th International Workshop on Description Logics (DL-2013). Vol. Vol-1014. RWTH Aachen University. 2013. p. 724-734. (CEUR Workshop Proceedings).

A Refined Tableau Calculus with Controlled Blocking for the Description Logic SHOI

Abstract

Publication series

Access to Document

Fingerprint

Cite this