# Item

ITEM ACTIONSEXPORT

Released

Thesis

#### Reasoning in Combinations of Theories

##### External Resource

http://scidok.sulb.uni-saarland.de/volltexte/2010/3472/

(Any fulltext)

http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de

(Copyright transfer agreement)

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

diss.pdf

(Any fulltext), 2MB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Ihlemann, C. (2010). Reasoning in Combinations of Theories. PhD Thesis, Universität des Saarlandes, Saarbrücken. doi:10.22028/D291-26011.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-144B-3

##### Abstract

Verification problems are often expressed in a language which mixes several

theories.

A natural question to ask is whether one can use decision procedures for

individual theories to construct a decision procedure for the union theory.

In the cases where this is possible one has a powerful method at hand to handle

complex theories effectively.

The setup considered in this thesis is that of one base theory which is

extended by one or more theories.

The question is if and when a given ground satisfiability problem in the

extended setting can be

effectively reduced to an equi-satisfiable

problem

over the base theory. A case where this reductive approach is always possible

is that of so-called \emph{local theory extensions.}

The theory of local extensions is developed and some applications concerning

monotone functions are given.

Then the theory of local theory extensions is generalized in order to deal with

data structures that

exhibit local behavior.

It will be shown that 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 \emph{modularity} result is given that under certain

circumstances the locality of each of the extensions

lifts to locality of the entire extension.

The reductive approach outlined above has become particularly relevant

in recent years due to the rise of powerful solvers for background

theories common in verification tasks. These so-called SMT-solvers

effectively handle theories such as real linear or integer arithmetic.

As part of this thesis, a program called \emph{\mbox{H-PILoT}} was

implemented which carries out reductive reasoning for local theory

extensions. H-PILoT found applications in mathematics, multiple-valued

logics, data-structures and reasoning in complex systems.

theories.

A natural question to ask is whether one can use decision procedures for

individual theories to construct a decision procedure for the union theory.

In the cases where this is possible one has a powerful method at hand to handle

complex theories effectively.

The setup considered in this thesis is that of one base theory which is

extended by one or more theories.

The question is if and when a given ground satisfiability problem in the

extended setting can be

effectively reduced to an equi-satisfiable

problem

over the base theory. A case where this reductive approach is always possible

is that of so-called \emph{local theory extensions.}

The theory of local extensions is developed and some applications concerning

monotone functions are given.

Then the theory of local theory extensions is generalized in order to deal with

data structures that

exhibit local behavior.

It will be shown that 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 \emph{modularity} result is given that under certain

circumstances the locality of each of the extensions

lifts to locality of the entire extension.

The reductive approach outlined above has become particularly relevant

in recent years due to the rise of powerful solvers for background

theories common in verification tasks. These so-called SMT-solvers

effectively handle theories such as real linear or integer arithmetic.

As part of this thesis, a program called \emph{\mbox{H-PILoT}} was

implemented which carries out reductive reasoning for local theory

extensions. H-PILoT found applications in mathematics, multiple-valued

logics, data-structures and reasoning in complex systems.