Campus Event Calendar
Event Entry
What and Who
Superposition and Model Evolution Combined
Peter Baumgartner and Uwe Waldmann
NICTA and Australan National University, Canberra, Australia
Talk
AG 1, AG 3, AG 4, AG 5, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 3 July 2009
11:00
-- Not specified --
E1 4
Rotunda, 6th floor (R633)
Saarbrücken
Abstract
Superposition and Model Evolution are calculi for automated
theorem proving in first-order logic. We present a new calculus,
ME+SUP, which generalizes both calculi (with equality) by integrating
their inference rules and redundancy criteria in a non-trivial
way. The main motivation is to combine the advantageous features of
both, rather complementary, calculi in a single framework. For
instance, Model Evolution, as a lifted version of the propositional
DPLL procedure, contributes a non-ground splitting rule that
effectively permits to split a clause into non variable disjoint
subclauses. In the talk I give an overview of the ME+Sup calculus
and the main ideas behind it.
theorem proving in first-order logic. We present a new calculus,
ME+SUP, which generalizes both calculi (with equality) by integrating
their inference rules and redundancy criteria in a non-trivial
way. The main motivation is to combine the advantageous features of
both, rather complementary, calculi in a single framework. For
instance, Model Evolution, as a lifted version of the propositional
DPLL procedure, contributes a non-ground splitting rule that
effectively permits to split a clause into non variable disjoint
subclauses. In the talk I give an overview of the ME+Sup calculus
and the main ideas behind it.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 07/01/2009 15:03 -- Created document.