Ozan Kahramanogullari 
-
ozank at doc dot ic dot ac dot uk -
Last updated on 28.06.2006
The Calculus of Structures in Maude
This web site is dedicated to the implementations of the logical
systems
in
the calculus of structures, mainly, in the language
Maude.
Within a
colaboration with the
Protheo group at
LORIA, we have
also developed
Java implementations using the pattern matching compiler
TOM.
NEW:
Max Schäfer
developed a graphical proof editor, called
GraPE,
for the Maude modules below.
By using GraPE, one can interactively construct proofs
in different systems of the calculus of structures.
GraPE is easy to install and fun to use.
The calculus of structures is a generalization of the
sequent calculus.
It was conceived by
Alessio Guglielmi
to express a logical system, called BV,
with a self-dual non-commutative connective resembling the
sequential composition
in process algebra. Apart from system BV, the calculus of structures
admits systems
also for existing logics such as
classical logic, linear logic and modal logics.
Besides other properties, one interesting
and important property
which distinguishes this formalism from the sequent
calculus is deep inference :
like in term rewriting, inference rules are deeply applicable
inside expressions.
This observation gives rise to the following question:
is it possible to express systems
in the calculus of structures as term rewriting systems
modulo an equational theory?
From the calculus of structures to term rewriting systems.
with Steffen Hölldobler
Technical Report WV-04-03, Knowledge Representation and Reasoning
Group, Artificial Intelligence Institute,
Department of Computer Science,
Dresden University of Technology, Dresden, Germany, 2004.
Download:
PDF file
Bib Tex entry
Having answered this question positively, I started looking for an
efficient implementation of
term rewriting systems which supports rewriting modulo equational
theories such as AC1 and A1.
After a short investigation and having asked some clever people
what they think about different
term rewriting platforms, Maude
has been the obvious choice: Maude has a built in
very fast matching algorithm
that supports different combinations of
associative,
commutative equational theories, also with
the presence of unit(s). Another important
feature of Maude that makes it a plausible platform for
implementing systems of the
calculus of structures is the availability of the search
function since the 2.0 release of Maude.
This function implements
breadth-first search which is vital for complete proof search.
Non-commutative Linear Logic
System BV
Although it is possible to express the existing systems
for Classical Logic and systems for all the fragments of Linear Logic
as Maude Modules, I have been experimenting mostly with
system BV.
System BV is an extension of multiplicative linear logic with the rules mix,
nullary mix, and a self-dual, non-commutative logical operator.
System BV is NP-complete,
System BV is NP-complete
in Proceedings of the
12th Workshop on Logic, Language, Information and Computation,
WoLLIC'05.
Florianapolis, Brazil, July 2005, Electronic Notes in Theoretical Computer Science.
Download: PDF file
Bib TeX entry
so if you are patient, it is possible to search
for proofs within the following Maude module for this logic.
Implementing System BV of the Calculus of Structures in Maude
In Proceedings of the ESSLLI-2004 Student Session,
Université Henri Poincaeé, Nancy, France
Download:
PDF file .
Bib Tex entry
The Maude Modules :
NNF
BV
I played around a little bit with the rules and the
equational theory of this system. Without providing
any strategy, the proof search can become much much faster
(100 times, and even more) in equivalent systems
where the rules are slightly manipulated in order to
remove the units from the structures.
This is because the redundant applications of some rules
are disabled, and rule applications with respect to unit become explicit.
The paper below is about these ideas.
System BV without the Equalities for Unit
in Proceedings of the ISCIS-2004
Download:
PDF file
Bib Tex entry
The Maude Modules :
NF
BVn
BVu
The nondeterminism in proof search can be reduced further by paying
attention to the mutual dependencies between dual atoms in a proof
search episode. The following paper is about these ideas:
Reducing the Nondeterminism in the Calculus of Structures,
accepted at LPAR'06
February, 2006
A preliminary version had been presented at the
ICCL Workshop
Proof Theory 2005,
TU Dresden,
February 2005
Conference version:
PDF file
Technical Report:
PS file
The Maude Module :
BVi
Here you can also find a prototype, which implements system BV in TOM,
following the ideas in the below paper.
Implementing Deep Inference in TOM
with
Pierre-Etienne Moreau
and
Antoine Reilles
accepted at the
Structures and Deduction Workshop 2005,
SD'05,
ICALP'05 Satellite, Lisbon, Portugal, July 2005
Download:
PDF file
PS file
Bib TeX entry
System NEL
System NEL
is an extension of multiplicative
exponential linear logic with the rules mix, nullary mix,
and a self-dual, non-commutative logical operator. In other words, system
NEL extends system BV with the exponentials of linear logic.
It was designed by
Alessio Guglielmi
and
Lutz Strassburger.
Although multiplicative exponential linear logic is unknown to
be decidable or not, NEL is shown to be
undecidable.
The Maude Modules :
ENF
NEL
UNF
NELn
By exploiting the self-dual, noncommutative logical operator of NEL,
I encoded the conjunctive planning problems in this logic.
This way, it became possible to observe partial order plans as
premises of computation derivations where the independence and
causality between actions is respected in the partial order.
In contrast to partial order planners in the literature,
this resulted in a planning formalism which admits a
noninterleaving concurrency semantics:
Labeled Event Structure Semantics of Linear Logic Planning
November, 2004
Presented at the
1st World Congress on Universal Logic,
Montreux, Switzerland,
March 31 - April 3, 2005
Short Abstract:
PDF file
Technical Report:
PDF file
Towards Planning as Concurrency
In Proceedings of the
AIA 2005
Download:
PDF file
Bib Tex entry
Based on the above paper, I had a lot of fun implementing the following planner.
NEL-PLANNER
Classical Logic
Kai Brünnler
wrote
his
Ph.D. thesis
on the classical logic in the
calculus of structures.
The Maude Modules :
NNF
KSg
UNF
KSgn
Due to the contraction rule, the system KS of
the calculus of structures cannot be implemented
without introducing a strategy. While looking for
a system that does not require an underlying
equational theory, I developed a system
that is similar to the sequent system G3, where
the equational theory becomes redundant.
Below is a short note on this system.
A System in the Calculus of Structures for
Classical Logic without Associativity and
Commutativity
Draft
Download:
PDF file.
The Maude Modules :
NNF
DKS
By employing the maude meta-level commands, I implemented
the above strategy in Maude. This way, the module became
plausible for more realistic applications.
In the above module, I prefered to use
associativity and commutativity since this allowed me
to accomplish the implementation by only using the
reduce fuction without using
the search function.
The Maude Module :
Strategic-DKS
(Maude 2.1 or later is required.)
Besides the Maude modules, there is also a Prolog implementation
of this system which does not work as good as the Maude module, but
there one can use n-ary structures, although in the Maude impementation
one can only input binary structures.
A Prolog Program that Implements this system
Works in SWI-Prolog or ECLiPSe Prolog.
Download: Source
Linear Logic
Lutz Strassburger
studied the proof theory of Linear Logic within
the calculus of structures in
his Ph. D. thesis.
The Maude Modules :
ENF
LS
The following paper is a note on orienting the equalities for unit in
the systems for linear logic in order to disable redundant application
of the inference rules.
System LS without the Equalities for Unit
Download:
PDF file
The Maude Modules :
UNF
LSn
Modal Logics
Charles Stewart
and
Phiniki Stouppa
are investigating the
modal logics in the calculus of structures.
I got these modules by orienting the equalities
[]tt = tt
<>ff = ff
from left to right as bottom-up proof-search rules. I believe that,
thisway, I do not lose completeness,
but I have not proved it.
Modal Logic M
The Maude Modules :
NNF
KS-M
