SUMMARY
For my Ph. D., I am developing a common language for
concurrency and planning
that aims at bringing these two fields closer.
Such a language will allow to transfer
mathematical notions from concurrency to planning,
and provide a platform for a
structural analysis of plans. For this purpose, I am using
the logical systems of the
recently developed proof theoretical
formalism, the calculus of structures.
This formalism admits
deductive systems which extend different fragments of linear
logic with a self-dual, non-commutative logical operator.
By resorting to these
systems, which can not be designed in
any standard sequent calculus, parallel and
sequential composition
of the developed language can be naturally expressed by
means of commutative and non-commutative logical operators. While
inference
rules of the proof theoretical systems provide an
operational semantics of the
language I develop, a behavioral
semantics is obtained by borrowing methods
from concurrency theory.
I am also implementing the proof search in these logical
systems. These
implementations do not only provide the tools for
the language developed, but
also assist the proof theoretical
research on different logics, i.e., classical logic,
modal logics,
linear logic, within this formalism. In order to reduce
nondeterminism in proof search, I develop new proof theoretical
techniques.
Besides making the above mentioned implementations
more efficient, these
techniques are used as combinatorial proof
theoretic tools while proving
properties of these logical systems.
my implementations web-site
my papers
Last updated on 19.05.2005