zbMATH — the first resource for mathematics

A tableau calculus for temporal description logic: The expanding domain case. (English) Zbl 1017.03007
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.

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