Campus Event Calendar
Event Entry
New for: D2, D3
What and Who
Saturation-Based Decision Procedures for Fixed Domain and Minimal Model Validity
Matthias Horbach
Max-Planck-Institut für Informatik - RG 1
Promotionskolloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 22 July 2010
14:00
60 Minutes
E1 4
019
Saarbrücken
Abstract
Superposition is an established decision procedure for a variety of
first-order logic theories. A satisfiable theory, saturated by superposition,
first-order logic theories. A satisfiable theory, saturated by superposition,
implicitly defines a minimal Herbrand model for the theory.
This raises the question in how far superposition calculi can be
employed for reasoning about such minimal models.
In this thesis, I propose the first superposition calculus that can
compute wrt. a minimal model and a fixed domain
semantics and that is sound and complete in the limit. Since
Skolemization is incomplete for these semantics, existentially
quantified variables are explicitly represented. Based on the calculus,
I present a number of decidability results for queries
with one quantifier alternation.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 07/16/2010 09:07 -- Created document.