PDL with Negation of Atomic Programs

C. LutzC. Lutz, D. WaltherD. Walther

Datei:LutzWaltherIJCAR04.ps.gz

Download

C. Lutz, D. Walther
PDL with Negation of Atomic Programs
Proceedings of the 2nd International Joint Conference on Automated Reasoning {IJCAR'04}, Lecture Notes in Artificial Intelligence, to appear. Springer

Details
Bibtex

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, it is long known that 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.
Bemerkung: Note: To appear
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ LutzWaltherIJCAR04,
  author = {C. {Lutz} and D. {Walther}},
  booktitle = {Proceedings of the 2nd International Joint Conference on Automated Reasoning {IJCAR'04}},
  note = {To appear},
  publisher = {Springer Verlag},
  series = {Lecture Notes in Artificial Intelligence},
  title = {PDL with Negation of Atomic Programs},
  year = {2004},
}