A Tableau Algorithm for the Clique Guarded Fragment

C. HirschC. Hirsch, Stephan TobiesStephan Tobies

Datei:HirschTobies-AiML-2000.ps.gz

Download

C. Hirsch, Stephan Tobies
A Tableau Algorithm for the Clique Guarded Fragment
Proceedings of the Workshop Advances in Modal Logic AiML 2000, 2000

Details
Bibtex

KurzfassungAbstract
We develop a tableau algorithm for the Clique Guarded Fragment (CGF), which we hope can serve as basis for an efficient implementation of a decision procedure for CGF. This hope is justified by the fact that some of the most efficient implementations of modal or description logic reasoners are based on tableau calculi similar to the one for CGF presented in this paper. As a corollary from the constructions used to prove the correctness of the tableau algorithm, we give an, in our opinion, simpler proof for the finite modal property of the Guarded Fragment (GF). An extension of our approach to CGF is part of future work. We also give a new proof of the fact that CGF and GF have the generalised tree model property.
Bemerkung: Note: Final version appeared in Advanced in Modal Logic Volume 3, 2001.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@inproceedings{ HirschTobies-AiML-2000,
  address = {Leipzig, Germany},
  author = {C. {Hirsch} and S. {Tobies}},
  booktitle = {Proceedings of the Workshop Advances in Modal Logic {AiML 2000}},
  note = {Final version appeared in Advanced in Modal Logic Volume 3, 2001.},
  title = {A Tableau Algorithm for the Clique Guarded Fragment},
  year = {2000},
}