Campus Event Calendar
Event Entry
What and Who
Saturation-Based Decision Procedures for Extensions of the Guarded Fragment
Yevgeny Kazakov
Max-Planck-Institut für Informatik - AG 2
Promotionskolloquium
AG 1, AG 2, AG 3, AG 4, AG 5
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 17 March 2006
16:30
-- Not specified --
46.1 - MPII
024
Saarbrücken
Abstract
Abstract:
We apply the framework of Bachmair and Ganzinger for saturation-based
theorem proving to derive a range of decision procedures for logical
formalisms, starting with a simple terminological language EL, which
allows for conjunction and existential restrictions only, and ending
with extensions of the guarded fragment with equality, constants,
functionality, number restrictions and compositional axioms of form S
o T < H. Our procedures are derived in a uniform way using standard
saturation-based calculi enhanced with simplification rules based on
the general notion of redundancy. We argue that such decision
procedures can be applied for reasoning in expressive description
logics, where they have certain advantages over traditionally used
tableau procedures, such as optimal worst-case complexity and direct
correctness proofs.
Titel:
Saturirungs-basierte Entscheidungsverfahren für Erweiterungen des
Guarded Fragments
Zusammenfassung:
Wir wenden das Framework von Bachmair und Ganzinger für
saturierungsbasiertes Theorembeweisen an, um eine Reihe von
Entscheidungsverfahren für logische Formalismen abzuleiten, angefangen
von einer simplen terminologischen Sprache
EL, die nur Konjunktionen und existentielle Restriktionen erlaubt, bis
zu Erweiterungen des Guarded Fragment mit Gleichheit, Konstanten,
funktionalität, Zahlenrestriktionen und Kompositionsaxiomen der Form S
o T < H. Unsere Verfaren sind einheitlich abgeleitet unter Benutzung
herkömmlicher saturierungsbasierter Kalküle, verbessert durch
Simplifikationsregeln, die auf der Konzept der Redundanz basieren. Wir
argumentieren, daß solche entscheidungsprozeduren für das Beweisen in
ausdrucksvoll Beschreibungslogiken angewendet werden können, wo sie
gewisse Vorteile gegenüber traditionell benutzten Tableauverfahren
besitzen, wie z.B. optimale worst-case Komplexität und direkt
Korrektheitsbeweise.
The talk will be in English.
We apply the framework of Bachmair and Ganzinger for saturation-based
theorem proving to derive a range of decision procedures for logical
formalisms, starting with a simple terminological language EL, which
allows for conjunction and existential restrictions only, and ending
with extensions of the guarded fragment with equality, constants,
functionality, number restrictions and compositional axioms of form S
o T < H. Our procedures are derived in a uniform way using standard
saturation-based calculi enhanced with simplification rules based on
the general notion of redundancy. We argue that such decision
procedures can be applied for reasoning in expressive description
logics, where they have certain advantages over traditionally used
tableau procedures, such as optimal worst-case complexity and direct
correctness proofs.
Titel:
Saturirungs-basierte Entscheidungsverfahren für Erweiterungen des
Guarded Fragments
Zusammenfassung:
Wir wenden das Framework von Bachmair und Ganzinger für
saturierungsbasiertes Theorembeweisen an, um eine Reihe von
Entscheidungsverfahren für logische Formalismen abzuleiten, angefangen
von einer simplen terminologischen Sprache
EL, die nur Konjunktionen und existentielle Restriktionen erlaubt, bis
zu Erweiterungen des Guarded Fragment mit Gleichheit, Konstanten,
funktionalität, Zahlenrestriktionen und Kompositionsaxiomen der Form S
o T < H. Unsere Verfaren sind einheitlich abgeleitet unter Benutzung
herkömmlicher saturierungsbasierter Kalküle, verbessert durch
Simplifikationsregeln, die auf der Konzept der Redundanz basieren. Wir
argumentieren, daß solche entscheidungsprozeduren für das Beweisen in
ausdrucksvoll Beschreibungslogiken angewendet werden können, wo sie
gewisse Vorteile gegenüber traditionell benutzten Tableauverfahren
besitzen, wie z.B. optimale worst-case Komplexität und direkt
Korrektheitsbeweise.
The talk will be in English.
Contact
Yevgeny Kazakov
--email hidden
passcode not visible
logged in users only
Veronika Weinand, 03/06/2006 14:33
Veronika Weinand, 03/03/2006 14:31 -- Created document.
Veronika Weinand, 03/03/2006 14:31 -- Created document.