Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
The equality elimination method
Andrei Voronkov
Logik-Seminar
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 17 June 97
17:00
-- Not specified --
46.1 - MPII
HS 024
Saarbrücken
Abstract
Equality elimination is a method of handling equality in automatic
theorem proving. Unlike the known paramodulation-based methods,
it is also applicable to rigid-variable methods (tableaux and
connections). In the case of the tableau method, equality elimination
results in a combination of backwards reasoning by the tableau method
and forward superposition-based reasoning.
theorem proving. Unlike the known paramodulation-based methods,
it is also applicable to rigid-variable methods (tableaux and
connections). In the case of the tableau method, equality elimination
results in a combination of backwards reasoning by the tableau method
and forward superposition-based reasoning.
In the talk, we shall describe the method and briefly survey other
methods of equality reasoning for rigid-variable methods.
All reported results have been obtained in collaboration with Anatoli
Degtyarev.
Contact
Uwe Waldmann
92-227
--email hidden
passcode not visible
logged in users only
Tags, Category, Keywords and additional notes
Vortragswuensche fuer das Logikseminar bitte an Uwe Waldmann, MPI,
Tel.: (0681) 9325-227, uni-intern: 92227
Uwe Brahm, 04/12/2007 12:43 -- Created document.