Algebraic and logical methods in automated theorem proving and in the study of concurrency

cumulative habilitation, no publication.

Vorstellungsvortrag
-------------------

Abstract:

The applications of algebra and logic in computer science are
particularly abundant nowadays; in fact logic is often called
"the calculus of computer science". On the other hand, the
development of computer science has a strong impact on the
research in algebra and logic, and in particular on the research
in computational mathematics and automated theorem proving.

\smallskip
In this talk I will present two, strongly interrelated, directions
of my recent research, which reflect some of the links between
algebra, logic and computer science emphasized above:

\begin{itemize}
\item Decompositions of algebraic structures in terms of simpler
structures, and applications to automated theorem proving.

\item A study of interaction in complex systems, and applications
to modular checking of certain properties of systems obtained
by composing simpler systems.
\end{itemize}


Antrittsvorlesung
-----------------

Abstract:

One of the most important problems in computer science is to
identify decidable and tractable fragments of (first- or
higher-order) logic, and to develop efficient deductive
calculi for these fragments.
However, in most real-life applications it is necessary to
consider combinations of theories which are, usually,
extensions of a shared base theory.
Two important questions arise in this context:

\begin{itemize}
\item Assume that we have a complete prover for a logical theory.
Can one use this prover as a ``black-box'' to prove theorems
in an extension of the theory?

\item Assume that we have complete provers for two theories.
Can we obtain a complete prover for their combination,
by using the provers of the components as ``black-boxes''?
\end{itemize}

In this talk we present several situations in which hierarchical
and modular reasoning is possible, and point out similarities
and differences between various approaches to modular theorem
proving in combinations of logical theories.

Theorem proving

Antrittsvorlesung, no publication.

Thema der Antrittsvorlesung: Automated reasoning in extensions and combinations of logical theories

November

2004