- Supervisor
- Viorica Sofronie - Max Planck Institut fuer Informatik, Saarbruecken
- Date and time
- Tuesday, May 8, 2007 at 5:00 PM - Inizio alle 17:30, CaffĂ¨, te e biscotti alle 17.
- Place
- Ca' Vignal - Piramide, Floor 0, Hall Verde
- Programme Director
- Maria Paola Bonacina
- External reference
- Publication date
- April 30, 2007
- Department

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.

© 2002 - 2021
Verona University

Via dell'Artigliere 8, 37129 Verona |
P. I.V.A. 01541040232 |
C. FISCALE 93009870234