Campus Event Calendar
Event Entry
What and Who
Superposition for Fixed Domains
Matthias Horbach
Max-Planck-Institut für Informatik - RG 1
RG1 Group Meeting
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 12 September 2008
11:00
30 Minutes
E1 4
Rotunda 6th floor
Saarbrücken
Abstract
Superposition is an established decision procedure for a variety of
first-order logic theories represented by sets of clauses. A satisfiable
theory, saturated by superposition, implicitly defines a minimal
term-generated model for the theory.
Proving universal properties with respect to a saturated theory directly
leads to a modification of the minimal model's term-generated domain, as
new Skolem functions are introduced. For many applications, this is not
desired.
Therefore, we propose the first superposition calculus that can
explicitly represent existentially quantified variables and can thus
compute with respect to a given domain. This calculus is sound and
complete for a first-order fixed domain semantics.
For some classes of formulas and theories, we can even employ the
calculus to prove properties of the minimal model itself, going beyond
the scope of known superposition based approaches.
first-order logic theories represented by sets of clauses. A satisfiable
theory, saturated by superposition, implicitly defines a minimal
term-generated model for the theory.
Proving universal properties with respect to a saturated theory directly
leads to a modification of the minimal model's term-generated domain, as
new Skolem functions are introduced. For many applications, this is not
desired.
Therefore, we propose the first superposition calculus that can
explicitly represent existentially quantified variables and can thus
compute with respect to a given domain. This calculus is sound and
complete for a first-order fixed domain semantics.
For some classes of formulas and theories, we can even employ the
calculus to prove properties of the minimal model itself, going beyond
the scope of known superposition based approaches.
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 09/10/2008 14:15 -- Created document.