LATPub189: Unterschied zwischen den Versionen

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Marcel Lippmann (Diskussion | Beiträge)
KKeine Bearbeitungszusammenfassung
 
Marcel Lippmann (Diskussion | Beiträge)
KKeine Bearbeitungszusammenfassung
 
(2 dazwischenliegende Versionen desselben Benutzers werden nicht angezeigt)
Zeile 2: Zeile 2:
|ErsterAutorVorname=C.
|ErsterAutorVorname=C.
|ErsterAutorNachname=Hirsch
|ErsterAutorNachname=Hirsch
|FurtherAuthors=S. Tobies
|FurtherAuthors=Stephan Tobies
}}
}}
{{Inproceedings
{{Inproceedings
Zeile 9: Zeile 9:
|Year=2000
|Year=2000
|Month=
|Month=
|Booktitle=Proceedings of the Workshop Advances in Modal Logic {AiML 2000}
|Booktitle=Proceedings of the Workshop Advances in Modal Logic AiML 2000
|Editor=
|Editor=
|Note=Final version appeared in Advanced in Modal Logic Volume 3, 2001.
|Note=Final version appeared in Advanced in Modal Logic Volume 3, 2001.
Zeile 20: Zeile 20:
}}
}}
{{Publikation Details
{{Publikation Details
|Abstract=We develop a tableau algorithm for the Clique Guarded Fragment (CGF), which we
|Abstract=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.
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.
 
|ISBN=
|ISBN=
|ISSN=
|ISSN=
Zeile 47: Zeile 37:
   year = {2000},
   year = {2000},
}
}
}}
}}

Aktuelle Version vom 25. März 2015, 16:34 Uhr

Toggle side column

A Tableau Algorithm for the Clique Guarded Fragment

C. HirschC. Hirsch,  Stephan TobiesStephan Tobies
C. Hirsch, Stephan Tobies
A Tableau Algorithm for the Clique Guarded Fragment
Proceedings of the Workshop Advances in Modal Logic AiML 2000, 2000
  • 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},
}