×

Tableaux for temporal description logic with constant domains. (English) Zbl 0988.68178

Goré, Rajeev (ed.) et al., Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2083, 121-136 (2001).
Summary: We show how to combine the standard tableau system for the basic description logic \(\mathcal{ALC}\) and Wolper’s tableau calculus for propositional temporal logic PTL (with the temporal operators ‘next-time’ and ‘until’) in order to design a terminating sound and complete tableau-based satisfiability-checking algorithm for the temporal description logic \(\text{PTL}_{\mathcal{ALC}}\) of 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)] interpreted in models with constant domains. We use the method of quasimodels to represent models with infinite domains, and the technique of minimal types to maintain these domains constant. The combination is flexible and can be extended to more expressive description logics or even to decidable fragments of first-order temporal logics.
For the entire collection see [Zbl 0968.00052].

MSC:

68T27 Logic in artificial intelligence
03B35 Mechanization of proofs and logical operations
03B44 Temporal logic
68T30 Knowledge representation

Citations:

Zbl 0994.03026
PDFBibTeX XMLCite
Full Text: Link