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

MPI-INF RG1 Publications :: Thesis :: Wischnewski, Patrick


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)*:Wischnewski, Patrick
BibTeX citekey*:Wischnewski2007
Language:English

Title, School
Title*:Contextual Rewriting in SPASS
School:Universität des Saarlandes
Type of Thesis*:Master's thesis
Year:2007

Publisher
Publishers Name:Self publishing

Note, Abstract, Copyright
LaTeX Abstract:
First-order theorem proving with equality is undecidable, in general.
However, it
is semi-decidable in the sense that it is refutationally complete. The
basis for a
(semi)-decision procedure for first-order clauses with equality is a
calculus composed
of inference and reduction rules. The inference rules of the calculus
generate
new clauses whereas the reduction rules delete clauses or transform them
into simpler
ones. If, in particular, strong reduction rules are available,
decidability of
certain subclasses of first-order logic can be shown. Hence,
sophisticated reductions
are essential for progress in automated theorem proving. In this thesis we
consider the superposition calculus and in particular the sophisticated
reduction
rule Contextual Rewriting. However, it is in general undecidable whether
contextual
rewriting can be applied. Therefore, to make the rule applicable in
practice,
it has to be further refined. In this work we develop an instance of
contextual
rewriting which effectively performs contextual rewriting and we
implement this
in the theorem prover Spass.
Download Access Level:Intranet

Referees, Status, Dates
1. Referee:Christoph Weidenbach
2. Referee:Holger Hermanns
Status:Completed
Date Kolloquium:18 January 2008

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{Wischnewski2007,
AUTHOR = {Wischnewski, Patrick},
TITLE = {Contextual Rewriting in SPASS},
PUBLISHER = {Self publishing},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {2007},
TYPE = {Master's thesis}
}



Entry last modified by Roxane Wetzel, 04/14/2008
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:33:30 PM
Revisions
6.
5.
4.
3.
2.
Editor(s)
Roxane Wetzel
Anja Becker
Roxane Wetzel
Roxane Wetzel
Roxane Wetzel
Edit Dates
14.04.2008 15:20:29
07.04.2008 11:15:55
25.01.2008 14:24:16
25.01.2008 13:03:59
21.01.2008 09:49:25