Campus Event Calendar
Event Entry
What and Who
PhD Application Talk: Contextual Rewriting in SPASS
Patrick Wischnewski
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 29 October 2007
08:00
480 Minutes
E1 4
024
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
Contact
IMPRS
225
--email hidden
passcode not visible
logged in users only
Lourdes Lara-Tapia, 10/26/2007 18:58 -- Created document.