- Titel
- A Tableau Calculus for Temporal Description Logic
- Untertitel
- The Constant Domain Case.
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-789811
- Schriftenreihe
- LTCS-Report
- Bandnummer
- 01-01
- Erstveröffentlichung
- 2001
- DOI
- https://doi.org/10.25368/2022.111
- Abstract (EN)
- 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 of [19] interpreted in models with constant domains. We use the method of quasimodels [17, 15] to represent models with infinite domains, and the technique of minimal types [11] to maintain these domains constant. The combination is flexible and can be extended to more expressive description logics or even do decidable fragments of first-order temporal logics.
- Freie Schlagwörter (DE)
- Domäne, ALN-Konzept, Beschreibungslogik, zeitliche Logik
- Freie Schlagwörter (EN)
- domain, ALN-concept, description logic, temporal logic
- Klassifikation (DDC)
- 004
- Klassifikation (RVK)
- ST 136
- Publizierende Institution
- Aachen University of Technology, Aachen
- Version / Begutachtungsstatus
- angenommene Version / Postprint / Autorenversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-789811
- Veröffentlichungsdatum Qucosa
- 24.05.2022
- Dokumenttyp
- Bericht
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0