An Abstract Tableau Calculus for the Description Logic SHOI Using Unrestricted Blocking and Rewriting

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

In Kazakov, Y. and Lembo, D. and Wolter, F. (eds), Proceedings of the 2012 International Workshop on Description Logics (DL-2012). CEUR Workshop Proceedings 846, CEUR-WS.org. BiBTeX, PDF.

This paper presents an abstract tableau calculus for the description logic SHOI. SHOI is the extension of ALC with singleton concepts, role inverse, transitive roles and role inclusion axioms. The presented tableau calculus is inspired by a recently introduced tableau synthesis framework. Termination is achieved by a variation of the unrestricted blocking mechanism that immediately rewrites terms with respect to the conjectured equalities. This approach leads to reduced search space for decision procedures based on the calculus. We also discuss restrictions of the application of the blocking rule by means of additional side conditions and/or additional premises.


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

Last modified: 16 Oct 14
Copyright © 2012 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk