Item

Abstract

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.