Tableaux for Temporal Description Logic with Constant Domain
From International Center for Computational Logic
Tableaux for Temporal Description Logic with Constant Domain
Carsten LutzCarsten Lutz, Holger SturmHolger Sturm, Frank WolterFrank Wolter, M. ZakharyaschevM. Zakharyaschev
Carsten Lutz, Holger Sturm, Frank Wolter, M. Zakharyaschev
Tableaux for Temporal Description Logic with Constant Domain
In Rajeev Goré and Alexander Leitsch and Tobias Nipkow, eds., Proceedings of the International Joint Conference on Automated Reasoning, Lecture Notes in Artifical Intelligence, 121-136, 2001. Springer
Tableaux for Temporal Description Logic with Constant Domain
In Rajeev Goré and Alexander Leitsch and Tobias Nipkow, eds., Proceedings of the International Joint Conference on Automated Reasoning, Lecture Notes in Artifical Intelligence, 121-136, 2001. Springer
- KurzfassungAbstract
We show how to combine the standard tableau system for the basic description logic 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 PTL_ALC 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. - Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@inproceedings{ LuStuWoZa-IJCAR-01,
address = {Siena, Italy},
author = {C. {Lutz} and H. {Sturm} and F. {Wolter} and M. {Zakharyaschev}},
booktitle = {Proceedings of the International Joint Conference on Automated Reasoning},
editor = {Rajeev {Gor\'e} and Alexander {Leitsch} and Tobias {Nipkow}},
number = {2083},
pages = {121--136},
publisher = {Springer Verlag},
series = {Lecture Notes in Artifical Intelligence},
title = {Tableaux for Temporal Description Logic with Constant Domain},
year = {2001},
}