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

Khodadadi, M., Schmidt, R. A. and Tishkovsky, D. (2013)

In Galmiche, D. and Larchey-Wendling, D. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2013). Lecture Notes in Computer Science, Vol. 8123, Springer, 188-202. BiBTeX, PDF (final version available via DOI link to Springer).

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.

A short version appears in Proceedings of the 26th International Workshop on Description Logics (DL-2013). CEUR Workshop Proceedings, Vol-1014, CEUR-WS.org, 724-734. PDF.

Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 23 Sep 13
Copyright © 2013 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk