Technical, Research Report
@TechReport
Technischer-, Forschungsbericht


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:









Author, Editor

Author(s):

Fietzke, Arnaud
Weidenbach, Christoph

dblp
dblp



Editor(s):





BibTeX Citekey*:

FietzkeWeidenbach2008

Language:

English

Title, Institution

Title*:

Labelled Splitting

Institution*:

MPI-INF RG1

Publishers or Institutions Address*:

MPI für Informatik, Campus E 1 4, 66123 Saarbrücken

Type:

Research Report

No, Year, pp.,

Number*:

MPI-I-2008-RG1-001

Pages*:

45

Month:

September

VG Wort
Pages*:


Year*:

2008

ISBN/ISSN:






DOI:




Note, Abstract, ©

Note:


(LaTeX) 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.

Categories / Keywords:


Copyright Message:


HyperLinks / References / URLs:


Personal Comments:


File Upload:


Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Audience:

Expert

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:
@TECHREPORT{FietzkeWeidenbach2008,
AUTHOR = {Fietzke, Arnaud and Weidenbach, Christoph},
TITLE = {Labelled Splitting},
YEAR = {2008},
TYPE = {Research Report},
INSTITUTION = {MPI-INF RG1},
NUMBER = {MPI-I-2008-RG1-001},
PAGES = {45},
ADDRESS = {MPI f{\"u}r Informatik, Campus E 1 4, 66123 Saarbr{\"u}cken},
MONTH = {September},
}


Entry last modified by Manuel Lamotte-Schubert, 07/03/2012
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Roxane Wetzel
Created
09/10/2008 02:48:22 PM
Revisions
3.
2.
1.
0.
Editor(s)
Manuel Lamotte-Schubert
Manuel Lamotte-Schubert
Manuel Lamotte-Schubert
Roxane Wetzel
Edit Dates
03.07.2012 08:15:49
25.03.2011 09:10:31
15.01.2009 14:00:04
10.09.2008 14:54:30
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section
MPI-I-2008-RG1-001.pdfMPI-I-2008-RG1-001.pdf
View attachments here: