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.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:78981 |
| Date | 24 May 2022 |
| Creators | Lutz, Carsten, Sturm, Holger, Wolter, Frank, Zakharyaschev, Michael |
| Publisher | Aachen University of Technology |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/acceptedVersion, doc-type:report, info:eu-repo/semantics/report, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | urn:nbn:de:bsz:14-qucosa2-785040, qucosa:78504 |
Page generated in 0.0022 seconds