de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Datenschutzhinweis Impressum Kontakt
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

Geometric Resolution: A Proof Procedure Based on Finite Model Search

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

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

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: http://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.