Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
  Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben
Konferenzbeitrag

A Superposition Decision Procedure for the Guarded Fragment with Equality

MPG-Autoren
/persons/resource/persons44474

Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44298

de Nivelle,  Hans
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

Ganzinger, H., & de Nivelle, H. (1999). A Superposition Decision Procedure for the Guarded Fragment with Equality. In G. Longo (Ed.), Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science (LICS-99) (pp. 295-303). Los Alamitos, USA: IEEE.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-000F-362C-2
Zusammenfassung
We give a decision procedure for the guarded fragment with equality. The procedure is based on resolution with superposition. The relevance of the guarded fragment lies in the fact that many modal logics can be translated into it. In this way the guarded fragment acts as a framework explaining some of the nice properties of these modal logics. By constructing an implementable decision procedure for the guarded fragments we define an effective procedure for deciding these modal logics. It is surprising to see that one does not need any sophisticated simplification and redundancy elimination method to make superposition terminate on the class of clauses that is obtained from the clausification of guarded formulas. Yet the decision procedure obtained is optimal with regard to time complexity.