A tableau calculus for temporal description logic: The expanding domain case. (English) Zbl 1017.03007

Sturm, Holger; Wolter, Frank

J. Log. Comput. 12, No. 5, 809-838 (2002).

The main concern of this paper is a detailed treatment of a tableau-based decision procedure for a certain temporalization of the description logic \({\mathcal ALC}.\) The latter is a widely accepted formalism representing knowledge in a time-independent way. The temporal extensions of \({\mathcal ALC}\) of the kind relevant to the present paper (i.e., with Until applicable to concepts and formulas) were introduced by F. Wolter and M. Zakharyaschev [“Temporalizing description logic”, in: D. M. Gabbay et al. (eds.), Frontiers of combining systems 2. Baldock: Research Studies Press, Stud. Log. Comput. 7, 379-401 (2000; Zbl 0994.03026)].
The authors confine themselves to the expanding domain case of their combined system. The algorithm they present is a sophisticated combination of the respective standard tableau procedures for the components. Soundness and completeness of the new tableau calculus are proved in the paper. Since the considered logic lacks the bounded domain property the completeness proof proceeds via quasi-models (see the reference above). The paper is completed by a concrete example showing how the calculus works.

Reviewer: Bernhard Heinemann (Hagen)

MSC:

03B44	Temporal logic
68T27	Logic in artificial intelligence
68T30	Knowledge representation
03B70	Logic in computer science

Keywords:

description logic; temporalization; tableau calculus; quasi-models