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

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Contextual Rewriting in SPASS
Speaker:Patrick Wischnewski
coming from:Max-Planck-Institut für Informatik - RG 1
Speakers Bio:
Event Type:Talk RG1 Group Meeting
Visibility:D1, RG1
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Friday, 26 October 2007
Duration:30 Minutes
Building:E1 4
Room:Rotunda 6th floor
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
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
rule Contextual Rewriting. However, it is in general undecidable whether
rewriting can be applied. Therefore, to make the rule applicable in
it has to be further refined. In this talk I present an instance of
rewriting which effectively performs contextual rewriting and show how this
can be implemented in the theorem prover SPASS.
Name(s):Roxane Wetzel
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Roxane Wetzel, 10/24/2007 02:00 PM -- Created document.