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
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
Public Audience

Date, Time and Location

Wednesday, 25 August 2010
60 Minutes
E1 4


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.


Jennifer Müller
--email hidden
passcode not visible
logged in users only

Jennifer Müller, 07/29/2010 11:25 -- Created document.