Implementation and evaluation of a tableau algorithm for the Guarded Fragment
From International Center for Computational Logic
Implementation and evaluation of a tableau algorithm for the Guarded Fragment
J. HladikJ. Hladik
J. Hladik
Implementation and evaluation of a tableau algorithm for the Guarded Fragment
In I. Horrocks and S. Tessaris, eds., Proceedings of the 2002 international workshop on description Logics (DL 2002), volume 53 of CEUR, 2002
Implementation and evaluation of a tableau algorithm for the Guarded Fragment
In I. Horrocks and S. Tessaris, eds., Proceedings of the 2002 international workshop on description Logics (DL 2002), volume 53 of CEUR, 2002
- KurzfassungAbstract
In this paper we present SAGA, an implementation of a tableau-based Satisfiability Algorithm for the Guarded Fragment (GF). Satisfiability for GF with finite signature is ExpTime-complete and therefore intractable in the worst case, but existing tableau-based systems for ExpTime-complete description and modal logics perform reasonably well for ``realistic knowledge bases. We implemented and evaluated several optimizations used in description logic systems, and our results show that, with an efficient combination, SAGA can compete with existing highly optimized systems for description logics. - Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@inproceedings{ Hladik-DL-2002,
address = {Toulouse, France},
author = {J. {Hladik}},
booktitle = {Proceedings of the 2002 international workshop on description Logics {(DL 2002)}},
editor = {I. {Horrocks} and S. {Tessaris}},
series = {CEUR},
title = {Implementation and evaluation of a tableau algorithm for the {G}uarded {F}ragment},
volume = {53},
year = {2002},
}
