Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Hochschulschrift

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

MPG-Autoren
/persons/resource/persons44660

Hustadt,  Ullrich
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe 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.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-000F-3545-0
Zusammenfassung
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.