Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF RG1 Publications :: Thesis :: Sofronie-Stokkermans, Viorica

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

Thesis - Habilitation thesis | | Habilitation(sschrift)

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

Title, School
Title*:Algebraic and logical methods in automated theorem proving and in the study of concurrency
School:Universität des Saarlandes
Type of Thesis*:Habilitation thesis

Note, Abstract, Copyright
Note:cumulative habilitation, no publication.
LaTeX Abstract:Vorstellungsvortrag



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.

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:

\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.



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:

\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''?

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.

Keywords:Theorem proving
Personal Comments:Antrittsvorlesung, no publication.
Download Access Level:Public
Download File(s):

Referees, Status, Dates
First Lecture Title:Thema der Antrittsvorlesung: Automated reasoning in extensions and combinations of logical theories
Date Kolloquium:24 November 2004

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

BibTeX Entry:
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.},

Entry last modified by Christine Kiesel, 03/20/2007
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Viorica Sofronie-Stokkermans
03/20/2007 10:13:35 AM
Christine Kiesel
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Edit Dates
27.04.2005 11:38:38
04/22/2005 03:08:16 PM
04/22/2005 03:05:58 PM
04/22/2005 03:03:29 PM