A program of LLP is a sequence of clauses (in fact, they are not clauses in the traditional sense). The syntax of clauses can be written in BNF as follows.

*C*, *G*, *R*, *S*, and *A* represent
``clause'', ``goal'', ``resource'',
``selective resource'', and ``atomic formula'' respectively.

Since the following equivalence relations are valid in linear logic, LLP compiler translates the left-hand side resource formula by the right-hand side.

Therefore, resource formulas can be rewritten as follows.

The order of the operator precedence is
```:-`'', ```;`'', ```&`'', ```,`'', ```-<>`'', ```!`''
from wider to narrower.
Newly introduced symbols to LLP (compared with Prolog) are
```&`'' (additive conjunction),
```-<>`'' (linear implication), ```!`'' (bang), and ```top`''.
LLP program not including these symbols can be executed as a Prolog
program.

Thu May 8 20:39:01 JST 1997