de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

Labelled splitting

MPS-Authors
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;

Locator
There are no locators available
Fulltext (public)

MPI-I-2008-RG1-001.pdf
(Any fulltext), 320KB

Supplementary Material (public)
There is no public supplementary material available
Citation

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.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-6674-D
Abstract
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.