LINK is a proof environment including proof nets-based provers
for multiplicative linear logics:
mixed linear logic, or
recently called non-commutative logic (MNL), commutative linear
logic (MLL)
and non-commutative (or cyclic) linear logic
(MCyLL). Its main characteristic is the study of provability
through automatic PROOF NETS construction.
The LINK proof engine is based on an algorithm of MLL Proof Nets
construction [1]
that has been adapted to deal with
non-commutative connectives (MCyLL) [2] and also with
both commutative and non-commutative connectives (MNL)
[3,4].
In case of MNL, three different algorithms are proposed. A first
one based on dependency graphs [4],
a second one
based on labels propagation [3] and a third one that adapts a
contractibility criterion,
initially dedicated to proof nets
verification and not to construction [5].
The first version of LINK was mainly written in OCaml by Luc
Habert, during its post-master degree
training period. New
versions, including improvements and optimisations, are under
development.
A short system description of LINK is given in
[6].
[1] D. Galmiche and G. Perrier A
procedure for automatic proof nets construction ,
Int. Conference on Logic Programming and Automated
Reasonning, LPAR'92,
LNAI 624, pp 42-53,
St. Petersburg, Russia, July, 1992.
[2] D. Galmiche and B. Martin
Proof nets construction and automated deduction in non-commutative
linear logic,
Electronic Notes in Theorical Computer
Science, vol 17, 1998
[3] D. Galmiche and J.-M. Notin
Proof-search and Proof nets in Mixed Linear Logic,
Electronic Notes in Theorical Computer Science, vol 37, 2000
[4] D. Galmiche and J.-M. Notin
Calculi with dependency relations for Mixed Linear Logic,
Int. Workshop on Logic and Complexity in Computer
Science, LCCS 2001,
Creteil, France, September 2001
[5] V. Mogbil Quadratic correctness criterion for
Non Commutative Logic,
15th Int. Workshop on Computer
Science Logic, CSL 2001,
LNCS 2142, pp 69-83, Paris,
France, September 2001
[6] L. Habert and J.-M. Notin and D. Galmiche
LINK: a Proof Environment based on Proof nets ,
Int. Conference on Analytic Tableaux and Related Methods,
TABLEAUX'02,
LNCS 2381, pp 330-334, Copenhagen, Danemark,
July 2002
LINK can be freely downloaded, copied, modified and
redistributed
under the terms of the GNU Public License,
version 2.
You must first download the archive (
here) of the sources, then extract the files
as follows
(under Unix and Linux) and compile it (you will need OCaml v3.02
or higher).
Then type (in a Unix shell):
tar xvzf Link-current.tar.gz
cd Link-1.02
make
After compiling the sources, you just have to type ./link in the directory where Link has been installed.
The file EXAMPLES in the Link directory contains examples of
provable and unprovable
formulae of MLL, MCyLL and MNL.
The file link.1 is the manual page of Link; type man -l
link.1 in a Unix shell to see it.
Logical connectives:
| ^ | unary not (postfix) |
| | | commutative multiplicative disjunction (par) |
| * | commutative multiplicative conjunction (times) |
| < | non-commutative multiplicative disjunction (sequential) |
| @ | non-commutative multiplicative conjunction (next) |
| -o | linear implication |
| -@ | non-commutative left linear implication |
| @- | non-commutative right linear implication |
Formulae are built up using basic syntactic units plus parentheses and whitespace.
| $mll | Switch to MLL proof net construction |
| $mcyll | Switch to MCyLL |
| $mnld | Switch to MNL (using dependencies - see [5]) |
| $mnlb | Switch to MNL (using beta_i labels - see [4]) |
| $mnlm | Switch to MNL (using contraction criterion - see [6]) |
| $step | Step by step construction, stoping
after each link is built, and displaying the progress in the graphic window. Just press a key in the graphic window to resume |
| $numbers | Number the links in the graphic window |
| $nostep | opposite to $step |
| $nonumbers | opposite to $numbers |