Implementation and Optimisation of a Tableau Algorithm for the Guarded Fragment

J. HladikJ. Hladik

Datei:Hladik-Tableaux-2002.ps.gz

Download

J. Hladik
Implementation and Optimisation of a Tableau Algorithm for the Guarded Fragment
In U. Egly and C. G. Fermüller, eds., Proceedings of the International Conference on Automated Reasoning with Tableaux and Related Methods (Tableaux 2002), volume 2381 of Lecture Notes in Artificial Intelligence, 2002. Springer

Details
Bibtex

KurzfassungAbstract
In this paper, we present SAGA, the implementation of a tableau-based Satisfiability Algorithm for the Guarded Fragment (GF). Satisfiability for GF with finite signature is Exptime-complete and therefore theoretically intractable, but existing tableau-based systems for Exptime-complete description and modal logics perform well for many realistic knowledge bases. We implemented and evaluated several optimisations used in description logic systems, and our results show that with an efficient combination, SAGA can compete with existing highly optimised systems for description logics and first order logic.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ hladik02-tab,
  author = {J. {Hladik}},
  booktitle = {Proceedings of the International Conference on Automated Reasoning with Tableaux and Related Methods (Tableaux 2002)},
  editor = {U. {Egly} and C. G. {Ferm\"uller}},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Artificial Intelligence},
  title = {Implementation and Optimisation of a Tableau Algorithm for the Guarded Fragment},
  volume = {2381},
  year = {2002},
}