Campus Event Calendar
Event Entry
What and Who
Contextual Rewriting in SPASS
Patrick Wischnewski
Max-Planck-Institut für Informatik - RG 1
Talk
AG 2, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 11 July 2008
11:00
30 Minutes
E1 4
Rotunda 6th floor
Saarbrücken
Abstract
Sophisticated reductions are an important means to achieve progress
in automated theorem proving. We consider the powerful reduction rule Contextual
Rewriting in the context of the superposition calculus. If the rule is
considered in its abstract, most general form, the applicability of contextual rewriting is not
decidable.
We develop a decidable instance of the general contextual rewriting
rule and implement it in SPASS. An experimental evaluation on the TPTP gives
first insights into the application potential of the rule instance.
in automated theorem proving. We consider the powerful reduction rule Contextual
Rewriting in the context of the superposition calculus. If the rule is
considered in its abstract, most general form, the applicability of contextual rewriting is not
decidable.
We develop a decidable instance of the general contextual rewriting
rule and implement it in SPASS. An experimental evaluation on the TPTP gives
first insights into the application potential of the rule instance.
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 07/07/2008 09:17 -- Created document.