LATPub650: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
||
| Zeile 1: | Zeile 1: | ||
{{Publikation Erster Autor | {{Publikation Erster Autor | ||
|ErsterAutorVorname= | |ErsterAutorVorname=Carsten | ||
|ErsterAutorNachname=Lutz | |ErsterAutorNachname=Lutz | ||
|FurtherAuthors= | |FurtherAuthors=Holger Sturm; Frank Wolter; M. Zakharyaschev | ||
}} | }} | ||
{{Techreport | {{Techreport | ||
| Zeile 15: | Zeile 15: | ||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract=We show how to combine the standard tableau system for the basic | |Abstract=We show how to combine the standard tableau system for the basic description logic ALC with Wolper's tableau calculus for propositional temporal logic PTL 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. | ||
description logic ALC with Wolper's tableau calculus for | |||
propositional temporal logic PTL 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. | |||
|ISBN= | |ISBN= | ||
|ISSN= | |ISSN= | ||
| Zeile 46: | Zeile 34: | ||
year = {2001}, | year = {2001}, | ||
} | } | ||
}} | }} | ||
Version vom 23. März 2015, 13:24 Uhr
A Tableau Calculus for Temporal Description Logic: The Constant Domain Case
Carsten LutzCarsten Lutz, Holger SturmHolger Sturm, Frank WolterFrank Wolter, M. ZakharyaschevM. Zakharyaschev
Carsten Lutz, Holger Sturm, Frank Wolter, M. Zakharyaschev
A Tableau Calculus for Temporal Description Logic: The Constant Domain Case
Technical Report, LuFG Theoretical Computer Science, RWTH Aachen, volume LTCS-01-01, 2001. LTCS-Report
A Tableau Calculus for Temporal Description Logic: The Constant Domain Case
Technical Report, LuFG Theoretical Computer Science, RWTH Aachen, volume LTCS-01-01, 2001. LTCS-Report
- KurzfassungAbstract
We show how to combine the standard tableau system for the basic description logic ALC with Wolper's tableau calculus for propositional temporal logic PTL 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. - Bemerkung: Note: See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
- Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@techreport{ LuStuWoZa-LTCS-01-01,
address = {Germany},
author = {C. {Lutz} and H. {Sturm} and F. {Wolter} and M. {Zakharyaschev}},
institution = {LuFG Theoretical Computer Science, RWTH Aachen},
note = {See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.},
number = {LTCS-01-01},
title = {A Tableau Calculus for Temporal Description Logic: The Constant Domain Case},
type = {LTCS-Report},
year = {2001},
}
