Max-Planck-Institut für Informatik
max planck institut
informatik
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
Language:English
Date, Time and Location
Date:Friday, 26 October 2007
Time:11:00
Duration:30 Minutes
Location:Saarbrücken
Building:E1 4
Room:Rotunda 6th floor
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.
Contact
Name(s):Roxane Wetzel
Phone:900
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):
  • Roxane Wetzel, 10/24/2007 02:00 PM -- Created document.