LATPub304: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
Marcel Lippmann (Diskussion | Beiträge) K (Textersetzung - „D. Walther“ durch „Dirk Walther“) |
||
| (3 dazwischenliegende Versionen desselben Benutzers werden nicht angezeigt) | |||
| Zeile 1: | Zeile 1: | ||
{{Publikation Erster Autor | {{Publikation Erster Autor | ||
|ErsterAutorVorname= | |ErsterAutorVorname=Carsten | ||
|ErsterAutorNachname=Lutz | |ErsterAutorNachname=Lutz | ||
|FurtherAuthors= | |FurtherAuthors=Dirk Walther | ||
}} | }} | ||
{{Article | {{Article | ||
| Zeile 12: | Zeile 12: | ||
|Note= | |Note= | ||
|Number=2 | |Number=2 | ||
|Pages=189 | |Pages=189-214 | ||
|Publisher= | |Publisher= | ||
|Volume=15 | |Volume=15 | ||
| Zeile 18: | Zeile 18: | ||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract= | |Abstract= Propositional dynamic logic (PDL) is one of the most successful variants of modal logic. To make it even more useful for applications, many extensions of PDL have been considered in the literature. A very natural and useful such extension is with negation of programs. Unfortunately, as long known, reasoning with the resulting logic is undecidable. In this paper, we consider the extension of PDL with negation of atomic programs, only. We argue that this logic is still useful, e.g. in the context of description logics, and prove that satisfiability is decidable and ExpTime-complete using an approach based on Buechi tree automata. | ||
|ISBN= | |ISBN= | ||
|ISSN= | |ISSN= | ||
| Zeile 47: | Zeile 36: | ||
year = {2005}, | year = {2005}, | ||
} | } | ||
}} | }} | ||
Aktuelle Version vom 26. März 2015, 19:33 Uhr
PDL with Negation of Atomic Programs
Carsten LutzCarsten Lutz, Dirk WaltherDirk Walther
Carsten Lutz, Dirk Walther
PDL with Negation of Atomic Programs
Journal of Applied Non-Classical Logic, 15(2):189-214, 2005
PDL with Negation of Atomic Programs
Journal of Applied Non-Classical Logic, 15(2):189-214, 2005
- KurzfassungAbstract
Propositional dynamic logic (PDL) is one of the most successful variants of modal logic. To make it even more useful for applications, many extensions of PDL have been considered in the literature. A very natural and useful such extension is with negation of programs. Unfortunately, as long known, reasoning with the resulting logic is undecidable. In this paper, we consider the extension of PDL with negation of atomic programs, only. We argue that this logic is still useful, e.g. in the context of description logics, and prove that satisfiability is decidable and ExpTime-complete using an approach based on Buechi tree automata. - Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@article{ LutzWaltherJANCL05,
author = {C. {Lutz} and D. {Walther}},
journal = {Journal of Applied Non-Classical Logic},
number = {2},
pages = {189--214},
title = {PDL with Negation of Atomic Programs},
volume = {15},
year = {2005},
}
