max planck institut
informatik

# Publications Master Template :: Thesis :: Sofronie-Stokkermans, Viorica

Publications Master Template
 Show all entries of: Action: this year (2019) last year (2018) two years ago (2017) Open in Notes login to update

## Thesis - Habilitation thesis | | Habilitation(sschrift)

Author(s)*: Sofronie-Stokkermans, Viorica Sofronie-Stokkermans-hab04 English

Title*: Algebraic and logical methods in automated theorem proving and in the study of concurrency Universität des Saarlandes Habilitation thesis November 2004

Note: 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. Public

Status: Completed Thema der Antrittsvorlesung: Automated reasoning in extensions and combinations of logical theories 24 November 2004

MPG Unit: Max-Planck-Institut für Informatik Programming Logics Group MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography, VG Wort

BibTeX Entry:
@PHDTHESIS{Sofronie-Stokkermans-hab04,
AUTHOR = {Sofronie-Stokkermans, Viorica},
TITLE = {Algebraic and logical methods in automated theorem proving and in the study of concurrency},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {2004},
TYPE = {Habilitation thesis}
MONTH = {November},
NOTE = {cumulative habilitation, no publication.},
}