de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch

Hilfe Wegweiser Impressum Kontakt Einloggen

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Hochschulschrift

Resolution-Based Decision Procedures for Subclasses of First-Order Logic

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44660

Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Hustadt, U. (1999). Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD Thesis, Universität des Saarlandes, Saarbrücken.

This thesis studies decidable fragments of first-order logic which are relevant to the field of non-classical logic and knowledge representation. We show that refinements of resolution based on suitable liftable orderings provide decision procedures for the subclasses $\CE^+$, $\overline{\mathrm{K}}$, and $\overline{\mathrm{DK}}$ of first-order logic. By the use of semantics-based translation methods we can embed the description logic $\mathcal{ALCR}$ and extensions of the basic modal logic $\mathsf{K}$ into fragments of first-order logic. We describe various decision procedures based on ordering refinements and selection functions for these fragments and show that a polynomial simulation of tableaux-based decision procedures for these logics is possible. In the final part of the thesis we develop a benchmark suite and perform an empirical analysis of various modal theorem provers.