Campus Event Calendar
Event Entry
What and Who
Contextual Rewriting in SPASS
Patrick Wischnewski
Max-Planck-Institut für Informatik - RG 1
Talk RG1 Group Meeting
AG 1, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 26 October 2007
11:00
30 Minutes
E1 4
Rotunda 6th floor
Saarbrücken
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 talk I
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 talk I present an instance of
contextual
rewriting which effectively performs contextual rewriting and show how this
can be implemented in the theorem prover SPASS.
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 talk I
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 talk I present an instance of
contextual
rewriting which effectively performs contextual rewriting and show how this
can be implemented in the theorem prover SPASS.
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 10/24/2007 14:00 -- Created document.