• The added line is THIS COLOR.
• The deleted line is THIS COLOR.
```[[Documentation]]
//[[Documentation]]

*Examples
*Example Programs

**Append
A number of example programs, including

append(c(1,c(2,c(3,n))),c(4,c(5,n)),result).
-those with just one or a few rules,
-encodings of various calculi (propositional logic, Petri Nets, lambda calculus, ambient calculus, etc.),
-state-space search using SLIM's nondeterministic execution (typical AI problems etc.),
-model checking (distributed and concurrent algorithms, protocol verification, etc.),
-graph visualization using UNYO-UNYO (fullerenes (C60) etc.),
-those using LMNtal Java's GUI,

and so on, can be found in

-The [[''ltl'' subdirectory>http://www.ueda.info.waseda.ac.jp/lmntal/demo/ltl/]] contains both programs and LTL formulas to model-check them.
-The [[''unyo'' subdirectory>http://www.ueda.info.waseda.ac.jp/lmntal/demo/unyo/]] contains programs to be run under the UNYO-UNYO visualizer.
//-The [[''wt'' subdirectory>http://www.ueda.info.waseda.ac.jp/lmntal/demo/wt/]] contains programs to be run with the LMNtal window toolkit of LMNtal Java.

Let us introduce some simple examples below.

**List Concatenation

Lists formed with c(cons) and n(il) constructors can be concatenated using the following two rules:

append(X,Y,Z), n(X)      :- Y=Z.
append(X,Y,Z), c(A,X1,X) :- c(A,Z1,Z), append(X1,Y,Z1).

result = append([1,2,3],[4,5]).
Let them rewrite the following initial state:

append(c(1,c(2,c(3,n))),c(4,c(5,n)),result).

RESULT: result(c(1,c(2,c(3,c(4,c(5,n)))))) with the two rules above.

The above initial state is written using the '''term abbreviation scheme''' explained [[here>Syntax]].  By using the term abbreviation scheme and the Prolog-like list syntax, the list concatenation program can be written also as:

Z=append([],    Y) :- Z=Y.
Z=append([A|X1],Y) :- Z=[A|append(X1,Y)].

result = append([1,2,3],[4,5]).

**Self-Organizing Loop
a(free,free),a(free,free),a(free,free),a(free,free),a(free,free),
a(free,free),a(free,free),a(free,free),a(free,free),a(free,free),
a(free,free),a(free,free),a(free,free),a(free,free),a(free,free),
a(free,free),a(free,free),a(free,free),a(free,free),a(free,free),
a(free,free),a(free,free),a(free,free),a(free,free).
free(A),free(B),a(A,C),a(D,B):-a(X,C),a(D,X).
RESULT: result=[1,2,3,4,5] with the two rules above.

**Self-Organizing Loops

Ten agents, each with two free hands, are going to hold hands with others.
Is it possible that some agent is left alone?

a(free,free), a(free,free), a(free,free), a(free,free), a(free,free),
a(free,free), a(free,free), a(free,free), a(free,free), a(free,free).

a(X,free),a(free,Y) :- a(X,C),a(C,Y).

RESULT: Twenty possible final configurations, which can be computed by running SLIM with the ''-nd'' (nondeterministic execution) option.  LaViT's ''State&#86;iewer'' will show you a state transition diagram of the problem.

**Vending Machine
{customer,a,one,one,five,hunger,hunger}.
{customer,b,five,hunger}.
{vending,choco,choco,choco,one,one}.
{customer,\$c,hunger,five},  {vending,\$v,choco,one,one}
:- {customer,\$c,choco,one,one},{vending,\$v,five}.
{customer,\$c,hunger,one,one,one},{vending,\$v,choco}
:- {customer,\$c,choco},             {vending,\$v,one,one,one}.

Two customers with different amounts of coins and hunger
Each chocolate costs three and
there are only two kinds of coins: one and five.
are buying chocolates from a vending machine.
Each chocolate costs three
and only two kinds of coins are considered: one and five.

Run in shuffle mode (type shuffle).
{customer,a,five,one,one,hunger,hunger}.  % Customer a has \$7 and wants to buy two chocolates
{customer,b,five,hunger}.                 % Customer b has \$5 and wants to buy one chocolate
{vending,choco,choco,choco,one,one}.      % Vending machine has 3 chocolates

{customer,\$c,hunger,five}, {vending,\$v,choco,one,one} :-
{customer,\$c,choco,one,one}, {vending,\$v,five}.
{customer,\$c,hunger,one,one,one}, {vending,\$v,choco} :-
{customer,\$c,choco}, {vending,\$v,one,one,one}.

LaViT with ''-nd'' will compute two possible final states:

RESULT 1: {customer,a,choco,choco,one},
{customer,b,choco,one,one},
{vending,five,five,one}, <RULES>
RESULT 2: {customer,a,hunger,hunger,five,one,one},   // Oops!
{customer,b,choco,one,one},
{vending,choco,choco,five}, <RULES>

Observe that applying each rule preserves
the total number of coins and chocolates within the system.

```