Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF RG1 Publications :: Thesis :: Fietzke, Arnaud


MPI-INF RG1 Publications
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update

Thesis - Master's thesis | @MastersThesis | Masterarbeit


Author
Author(s)*:Fietzke, Arnaud
BibTeX citekey*:Fietzke2007
Language:English

Title, School
Title*:Labelled Splitting
School:Universität des Saarlandes
Type of Thesis*:Master's thesis
Month:October
Year:2007


Note, Abstract, Copyright
LaTeX Abstract:Saturation-based theorem provers are typically based on a calculus
consisting of inference and reduction rules that operate on sets of
clauses. While inference rules produce new clauses, reduction rules
allow the removal or simplification of redundant clauses and are an
essential ingredient for efficient implementations.
 The power of reduction rules can be further amplified by the use of
the splitting rule, which is based on explicit case analysis on variable-
disjoint components of a clause.
 In this thesis, I give a formalization of splitting and backtracking for
first-order logic using a labelling scheme that annotates clauses and
clause sets with additional information, and I present soundness and
completeness results for the corresponding calculus.
 The backtracking process as formalized here generalizes optimizations
that are currently being used, and I present the results of integrating
the improved backtracking into SPASS.
Download Access Level:Intranet

Referees, Status, Dates
1. Referee:Bernd Finkbeiner
2. Referee:Christoph Weidenbach
Status:Completed
Date Kolloquium:18 September 2019

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:

@MASTERSTHESIS{Fietzke2007,
AUTHOR = {Fietzke, Arnaud},
TITLE = {Labelled Splitting},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {2007},
TYPE = {Master's thesis}
MONTH = {October},
}



Entry last modified by Manuel Lamotte-Schubert, 03/25/2011
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
01/18/2008 03:38:36 PM
Revisions
5.
4.
3.
2.
1.
Editor(s)
Manuel Lamotte-Schubert
Manuel Lamotte-Schubert
Roxane Wetzel
Roxane Wetzel
Roxane Wetzel
Edit Dates
25.03.2011 09:10:59
15.01.2009 13:58:32
28.01.2008 08:51:45
25.01.2008 13:04:14
21.01.2008 13:58:41