A long term goal of the research in computer science is the
analysis and verification of complex systems. These can be
theories of mathematics, programs, reactive oder hybrid systems,
or large databases. Correctness proofs for such systems can
often be reduced to reasoning in complex logical theories
(e.g. combinations of numerical theories, theories of data
types, certain theories of functions). As the resulting proof
tasks are usually large, it is extremely important to have
efficient decision procedures.
In this talk we discuss situations in which efficient reasoning
in complex theories is possible. We consider a special type of
extensions of a base theory, which we call local extensions,
where hierarchic reasoning is possible (i.e., we can reduce the
task of proving satisfiability of (ground) formulae in the
extension to proving satisfiability of formulae in the base theory).
We give several examples of theories important for computer
science or mathematics which have this property. We show that the
decidability (and complexity) of the universal fragment of a local
theory extension can be expressed in terms of the decidability
(resp. complexity) of a suitable fragment of the base theory.
We briefly mention possibilities of modular reasoning in combinations
of local theory extensions, as well as possibilities of obtaining
interpolants in a hierarchical manner, and discuss applications in
verification and in knowledge representation.
CSS e script comuni siti DOL - frase 9957