Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
  Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben
Konferenzbeitrag

Geometric Resolution: A Proof Procedure Based on Finite Model Search

MPG-Autoren
/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

de Nivelle, H., & Meng, J. (2006). Geometric Resolution: A Proof Procedure Based on Finite Model Search. In Automated reasoning : Third International Joint Conference, IJCAR 2006 (pp. 303-317). Berlin, Germany: Springer.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-000F-2304-A
Zusammenfassung
We present a proof search procedure which is complete for first-order logic, but which also can be used when searching for finite models. The procedure uses a normal form that is closely related to geometric formulas. For this reason, we call the procedure geometric resolution. We expect that the procedure can be used as an efficient proof search procedure for first-order logic. We will point out how the procedure can be implemented in such a way that it is complete for finite models without loosing completeness for unsatisfiability. We will also discuss two refinements of the initial procedure, namely subsumption and functional reduction, and prove their completeness. Finally, we will discuss how the calculus can be implemented.