Campus Event Calendar
Event Entry
New for: D2, D3
What and Who
Reasoning in Combinations of Theories
Carsten Ihlemann
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
Wednesday, 25 August 2010
16:00
60 Minutes
E1 4
024
Saarbrücken
Abstract
Many problems in mathematics and computer science can be reduced to proving
the satisfiability of conjunctions of literals in a background theory
which can itself be a combination of theories.
So-called local theory extensions allow for hierarchical
reasoning: A given ground satisfiability problem in the extended
setting is effectively reduced to an equi-satisfiable problem over the
base theory.
In this thesis, the theory of local extensions is developed and some
applications are given. Further, the theory of local theory
extensions is generalized in order to deal with data structures that
exhibit local behavior: A suitable fragment of
both the theory of arrays and the theory of pointers is local in this
broader sense. Finally, the case of more than one theory extension is
discussed. In
particular, a modularity result is given that under certain
circumstances the locality of each of the extensions lifts to locality
of the entire extension.
the satisfiability of conjunctions of literals in a background theory
which can itself be a combination of theories.
So-called local theory extensions allow for hierarchical
reasoning: A given ground satisfiability problem in the extended
setting is effectively reduced to an equi-satisfiable problem over the
base theory.
In this thesis, the theory of local extensions is developed and some
applications are given. Further, the theory of local theory
extensions is generalized in order to deal with data structures that
exhibit local behavior: A suitable fragment of
both the theory of arrays and the theory of pointers is local in this
broader sense. Finally, the case of more than one theory extension is
discussed. In
particular, a modularity result is given that under certain
circumstances the locality of each of the extensions lifts to locality
of the entire extension.
Contact
Jennifer Müller
900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 07/29/2010 11:25 -- Created document.