English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

Labelled splitting

MPS-Authors
/persons/resource/persons44415

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

/persons/resource/persons45719

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

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
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: https://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.