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

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Labelled splitting

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

Fietzke,  Arnaud Luc
Automation of Logic, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45719

Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)

MPI-I-2008-RG1-001.pdf
(beliebiger Volltext), 320KB

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

Fietzke, A. L., & Weidenbach, C.(2008). Labelled splitting (MPI-I-2008-RG1-001). Saarbrücken: Max-Planck-Institut für Informatik. Retrieved from http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2008-RG1-001.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0014-6674-D
Zusammenfassung
We define a superposition calculus with explicit splitting and an explicit, new backtracking rule on the basis of labelled clauses. For the first time we show a superposition calculus with explicit backtracking rule sound and complete. The new backtracking rule advances backtracking with branch condensing known from SPASS. An experimental evaluation of an implementation of the new rule shows that it improves considerably the previous SPASS splitting implementation. Finally, we discuss the relationship between labelled first-order splitting and DPLL style splitting with intelligent backtracking and clause learning.