ausblenden:
Schlagwörter:
-
Zusammenfassung:
Many problems occurring in verification can be reduced to
proving the satisfiability of conjunctions of literals in a
background theory. This can be a concrete theory (e.g. the
theory of real or rational numbers), the extension of a
theory with additional functions (free, monotone, or
recursively defined) or a combination of theories. It is
therefore very important to have efficient procedures for
checking the satisfiability of conjunctions of ground
literals in such theories.
We present some new results on hierarchical and modular
reasoning in complex theories, as well as several examples
of application domains in which efficient reasoning is
possible. We show, in particular, that various phenomena
analyzed in the verification literature can be explained
in a unified way using the notion of local theory extension.
