//[[Documentation]] *Example Programs A number of example programs, including -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 [[''this directory'' (click here)>http://www.ueda.info.waseda.ac.jp/lmntal/demo/]]. -The 'ltl' subdirectory contains both programs and LTL formulas to model-check them. -The 'unyo' subdirectory contains programs to be run under the UNYO-UNYO visualizer. -The 'wt' subdirectory contains programs to be run with the LMNtal window toolkit of LMNtal Java. All these programs are included in the latest distribution of [[LaViT>http://www.ueda.info.waseda.ac.jp/lmntal/lavit/index.php?Download]]. 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). Enter those rules with 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 further applying 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]). 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. You can randomly compute them by running the program using LMNtal Java with the ''-s'' (shuffle) option, or running SLIM with the ''-nd'' (nondeterministic execution) option. LaViT's ''StateViewer'' will show you a state transition diagram of the problem. **Vending Machine Two customers with different amounts of coins and hunger are buying chocolates from a vending machine. Each chocolate costs three and only two kinds of coins are considered: one and five. {customer,a,five,one,one,hunger,hunger}. % Customer a has $7, buying 2 chocolates {customer,b,five,hunger}. % Customer b has $5, buying 1 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}, {customer,b,choco,one,one}, {vending,choco,choco,five}, <RULES> Observe that applying each rule preserves the total amount of coins and chocos within the system.