Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 5, October 2002: pp. 809-838

A Tableau Calculus for Temporal Description Logic: the Expanding Domain Case

Holger Sturm1 and Frank Wolter1

1Institut für Informatik, Universität Leipzig, Augustus-Platz 10-11, 04109 Leipzig, Germany. E-mail: {hsturm,wolter}@informatik.uni-leipzig.de

In this paper we present a tableau calculus for a temporal extension of the description logic ALC, called TLALC. This logic is based on the temporal language with 'Until' interpreted over the natural numbers with expanding ALC-domains. The tableau calculus forms an elaborate combination of Wolper's tableau calculus for propositional linear temporal logic, the standard tableau-algorithm for ALC, and the method of quasimodels introduced by Wolter and Zakharyaschev. Based on those three ingredients the paper provides a new method of how tableau-based decision procedures can be constructed for many-dimensional logics which lack the finite model property. The method can be applied to deal with other temporalized formalisms as well.

Keywords: Ten-point logic; description logic; tableau calculus; decision procedure

Table of Contents   Full-Text PDF (306 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement