% fib(N,F) <- F is the N-th Fibonacci number % inefficient doubly-recursive version fib(1,1). fib(2,1). fib(N,F):- N>2,N1 is N-1,N2 is N-2, fib(N1,F1),fib(N2,F2), F is F1+F2. /** <examples> ?- fib(5,F). ?- fib(10,F). ?- fib(20,F). ?- fib(25,F). ?- fib(30,F). */
fib/2 that returns an uninterpreted arithmetic expression showing the computation tree.
% :-use_rendering(svgtree). % uncomment this line to see visualisations % fibt(N,E) <- E is an arithmetic expression % representing the N-th Fibonacci number % that can be rendered as a tree % and evaluated with is/2. fibt(1,1). fibt(2,1). fibt(N,(F1+F2)):- N>2,N1 is N-1,N2 is N-2, fibt(N1,F1),fibt(N2,F2). /** <examples> ?- fibt(5,E), F is E. ?- fibt(10,E), F is E. */
% fibn(N,Na,Nb,F) <- F is the N-th Fibonacci number % in the sequence starting with Na, Nb fibn(1,Na,_,Na). fibn(2,_,Nb,Nb). fibn(N,Na,Nb,F):- N>2, N1 is N-1, Nc is Na+Nb, fibn(N1,Nb,Nc,F). % the original Fibonacci sequence starts with 1, 1 fibn(N,F):- fibn(N,1,1,F). /** <examples> ?- member(N,[10,20,50,100,200]), fibn(N,F). ?- maplist(fibn, [10,20,50,100,200], L). */
biglist(Low,High,L):-
bagof(X,between(Low,High,X),L).
% between/3 is built-in but could have been defined as follows:
% between(Low,_High,Low).
% between(Low,High,Number):-
% Low < High,
% NewLow is Low+1,
% between(NewLow,High,Number).
/** <examples>
?- biglist(1,25,L).
*/
:-use_module(library(random)). % for randseq/3 to generate random lists
setof_sort(In,Out):-
setof(X,member(X,In),Out).
/** <examples>
?- randseq(20,100,In), setof_sort(In,Out).
*/
% list of pairs p1(L,X,Y):- bagof((X,Y),(between(1,3,X),between(X,3,Y)),L). % one list for each X p2(L,X,Y):- bagof(Y,(between(1,3,X),between(X,3,Y)),L). % lists for each X combined p3(L,X,Y):- bagof(Y,X^(between(1,3,X),between(X,3,Y)),L). % one list for each Y p4(L,X,Y):- bagof(X,(between(1,3,X),between(X,3,Y)),L). % lists for each Y combined p5(L,X,Y):- bagof(X,Y^(between(1,3,X),between(X,3,Y)),L). /** <examples> ?- p1(L,X,Y). ?- p2(L,X,Y). ?- p3(L,X,Y). ?- p4(L,X,Y). ?- p5(L,X,Y). */
% :-use_rendering(chess). % Uncomment this line for chess renderer
nqueens(N,Columns) :-
setof(X,between(1,N,X),Rows),
perm(Rows,Columns), % generator
safe(Columns). % tester
%%% tester
safe([]).
safe([Column|Columns]) :-
noattack(Column,Columns,1),
safe(Columns).
noattack(_,[],_).
noattack(Y,[Y1|Ylist],Xdist) :-
abs(Y-Y1) =\= Xdist,
Xdist1 is Xdist+1,
noattack(Y,Ylist,Xdist1).
%%% generator
perm([],[]).
perm(L,[X|PR]):-
remove_one(X,L,R),
perm(R,PR).
remove_one(X,[X|Ys],Ys).
remove_one(X,[Y|Ys],[Y|Zs]):-
remove_one(X,Ys,Zs).
/** <examples>
?- nqueens(8,Columns).
*/
% factors(N,Fs) <- Fs is the list of prime factors of N factors(1,[1]). factors(X,[Factor|Fs]) :- X > 1, between(2,X,Factor), % generate candidate factor, lowest first (X mod Factor) =:= 0, % test Factor is divisor of X !, % if so, stop generating! Rem is X // Factor, % proceed with remainder factors(Rem,Fs). /** <examples> ?-factors(27,Fs). ?-factors(28,Fs). ?-factors(29,Fs). */
:-use_module(library(random)). % for randseq/3 to generate random lists
% psort(L,SL) <- L and SL contain the same elements, SL is sorted
psort(L,SL):-
perm(L,SL), % generator
write('. '), % demonstrate inefficiency of generator
sorted(SL). % tester
% perm(L,PL) <- L and PL are permutations of each other
perm([],[]).
perm(L,[X|PR]):-
remove_one(X,L,R),
perm(R,PR).
% remove_one(X,Ys,Zs) <- Zs is Ys minus one occurence of X
remove_one(X,[X|Ys],Ys).
remove_one(X,[Y|Ys],[Y|Zs]):-
remove_one(X,Ys,Zs).
% sorted(L) <- L is a sorted list
sorted([]).
sorted([_X]).
sorted([X,Y|L]):-
( compare('=', X, Y)
; compare('<', X, Y)
), sorted([Y|L]).
/** <examples>
?- randseq(5,100,In), psort(In,Out).
*/
prove(A):-
( A=true -> true % we're done
; A=not(B) -> not(prove(B)) % negation as failure
; A=(B,C) -> prove(B),prove(C) % conjunctive query
; otherwise -> cl(A,B),prove(B) % resolve against clause
).
% cl(H,B) <- (H:-B) is object-level clause
cl(rectangle,(polygon(4),angles(90))).
cl(square,(rectangle,regular)).
cl(triangle,polygon(3)).
cl(equilateral_triangle,(triangle,regular)).
%%% facts
cl(polygon(4),true).
cl(regular,true).
cl(angles(90),true).
/** <examples>
?- prove(rectangle).
?- prove(square).
?- prove(not(triangle)).
?- prove(not((rectangle,triangle))).
*/
prove_r(A):-
writeln(A), % show current query
( A=true -> true
; A=not(B) -> not(prove_r(B))
; A=(B,C) -> cl(B,D),conj_append(D,C,E),prove_r(E)
; otherwise -> cl(A,B),prove_r(B)
).
conj_append(A,B,C):-
( A=true -> B=C
; A=(A1,A2) -> C=(A1,C2),conj_append(A2,B,C2)
; otherwise -> C=(A,B)
).
% cl(H,B) <- (H:-B) is object-level clause
cl(rectangle,(polygon(4),angles(90))).
cl(square,(rectangle,regular)).
cl(triangle,polygon(3)).
cl(equilateral_triangle,(triangle,regular)).
%%% facts
cl(polygon(4),true).
cl(regular,true).
cl(angles(90),true).
/** <examples>
?- prove_r(rectangle).
?- prove_r(square).
?- prove_r(not(triangle)).
?- prove_r(not((rectangle,triangle))).
*/
% display a proof tree
prove_p(A):-prove_p(A,P),write_proof(P).
prove_p(A,P):-
( A=true -> P=[]
; A=(B,C) -> cl(B,D),conj_append(D,C,E),
prove_p(E,PE),P=[p(A,(B:-D))|PE]
; otherwise -> cl(A,B),prove_p(B,PB),
P=[p(A,(A:-B))|PB]
).
write_proof([]):-
write('...............[]'),nl.
write_proof([p(A,B)|Proof]):-
write((:-A)),nl,
write('.....|'),write('..........'),write(B),nl,
write('.....|'),write('..................../'),nl,
write_proof(Proof).
conj_append(A,B,C):-
( A=true -> B=C
; A=(A1,A2) -> C=(A1,C2),conj_append(A2,B,C2)
; otherwise -> C=(A,B)
).
% cl(H,B) <- (H:-B) is object-level clause
cl(rectangle,(polygon(4),angles(90))).
cl(square,(rectangle,regular)).
cl(triangle,polygon(3)).
cl(equilateral_triangle,(triangle,regular)).
%%% facts
cl(polygon(4),true).
cl(regular,true).
cl(angles(90),true).
/** <examples>
?- prove_p(rectangle).
?- prove_p(square).
*/
search_df([Goal|_Rest],Goal):- goal(Goal). search_df([Current|Rest],Goal):- %writeln([Current|Rest]), findall(C,child(Current,C),Children), append(Children,Rest,NewAgenda), search_df(NewAgenda,Goal). goal(N):-7 is N. goal(N):-42 is N. child(N,N+1). child(N,2*N). /** <examples> ?- search_df([0],Goal). ?- search_df([0],Goal),42 is Goal. */
search_bt(Goal,Goal):- goal(Goal). search_bt(Current,Goal):- %writeln(Current), child(Current,Child), search_bt(Child,Goal). goal(N):-7 is N. goal(N):-42 is N. child(N,N+1). child(N,2*N). /** <examples> ?- search_bt(0,Goal). ?- search_bt(0,Goal),42 is Goal. */
search_d(_D,Goal,Goal):- goal(Goal). search_d(D,Current,Goal):- %writeln(Current), D>0,D1 is D-1, child(Current,Child), search_d(D1,Child,Goal). goal(N):-7 is N. goal(N):-42 is N. child(N,N+1). child(N,2*N). /** <examples> ?- search_d(8,0,Goal). ?- search_d(8,0,Goal),42 is Goal. */
search_id(D,Current,Goal):- search_d(D,Current,Goal). search_id(D,Current,Goal):- %writeln(Current), D1 is D+1, % increase depth search_id(D1,Current,Goal). search_d(_D,Goal,Goal):- goal(Goal). search_d(D,Current,Goal):- D>0,D1 is D-1, child(Current,Child), search_d(D1,Child,Goal). goal(N):-7 is N. goal(N):-42 is N. child(N,N+1). child(N,2*N). /** <examples> ?- search_id(1,0,Goal). ?- search_id(1,0,Goal),42 is Goal. */
% hanoi(N,A,B,C,Moves) <- Moves is the list of moves to % move N disks from peg A to peg C, % using peg B as intermediary peg hanoi(0,_,_,_,[]). hanoi(N,A,B,C,Moves):- N>0, N1 is N-1, hanoi(N1,A,C,B,Moves1), hanoi(N1,B,A,C,Moves2), append(Moves1,[A -> C|Moves2],Moves). hanoi(N,Moves):- hanoi(N,left,middle,right,Moves). /** <examples> ?- hanoi(3,Moves). ?- hanoi(5,Moves). */
search_bf([Goal|_Rest],Goal):- goal(Goal). search_bf([Current|Rest],Goal):- %writeln([Current|Rest]), findall(C,child(Current,C),Children), append(Rest,Children,NewAgenda), search_bf(NewAgenda,Goal). goal(N):-7 is N. goal(N):-42 is N. child(N,N+1). child(N,2*N). /** <examples> ?- search_bf([0],Goal). ?- search_bf([0],Goal),42 is Goal. */
% breadth-first version of prove_r/1
% agenda items have the form a(CurrentQuery,OriginalQuery)
% in order to obtain an answer substitution on termination
prove_bf(Goal):-
prove_bf_a([a(Goal,Goal)],Goal).
prove_bf_a([a(true,Goal)|_Agenda],Goal).
prove_bf_a([a((A,B),G)|Agenda],Goal):-!,
findall(a(D,G),
(cl(A,C),conj_append(C,B,D)),
Children),
append(Agenda,Children,NewAgenda), % breadth-first
prove_bf_a(NewAgenda,Goal).
prove_bf_a([a(A,G)|Agenda],Goal):-
findall(a(B,G),cl(A,B),Children),
append(Agenda,Children,NewAgenda), % breadth-first
prove_bf_a(NewAgenda,Goal).
% prove_r/1 included for comparison
prove_r(A):-
( A=true -> true
; A=(B,C) -> cl(B,D),conj_append(D,C,E),prove_r(E)
; otherwise -> cl(A,B),prove_r(B)
).
cl(brother(X,Y),brother(Y,X)).
cl(brother(X,Y),(brother(X,Z),brother(Z,Y))).
cl(brother(peter,paul),true).
cl(brother(adrian,paul),true).
%%% auxiliary predicates
conj_append(A,B,C):-
( A=true -> B=C
; A=(A1,A2) -> C=(A1,C2),conj_append(A2,B,C2)
; otherwise -> C=(A,B)
).
/** <examples>
?- prove_bf(brother(peter,paul)).
?- prove_r(brother(peter,paul)).
?- prove_bf(brother(peter,Y)).
?- prove_r(brother(peter,Y)).
*/
% refute_bf(Clause) <- Clause is refuted by clauses
% defined by cl/1
% (breadth-first search strategy)
refute_bf(Clause):-
refute_bf_a([a(Clause,Clause)],Clause).
refute_bf_a([a((false:-true),Clause)|_Rest],Clause).
refute_bf_a([a(A,C)|Rest],Clause):-
writeln(A),
findall(a(R,C),(cl(Cl),resolve(A,Cl,R)),Children),
append(Rest,Children,NewAgenda), % breadth-first
refute_bf_a(NewAgenda,Clause).
% resolve(C1,C2,R) <- R is the resolvent of C1 and C2.
resolve((H1:-B1),(H2:-B2),(ResHead:-ResBody)):-
resolve(H1,B2,R1,R2),
disj_append(R1,H2,ResHead),
conj_append(B1,R2,ResBody).
resolve((H1:-B1),(H2:-B2),(ResHead:-ResBody)):-
resolve(H2,B1,R2,R1),
disj_append(H1,R2,ResHead),
conj_append(R1,B2,ResBody).
resolve((A;B),C,B,E):-
conj_remove_one(A,C,E).
resolve((A;B),C,(A;D),E):-
resolve(B,C,D,E).
resolve(A,C,false,E):-
conj_remove_one(A,C,E).
cl((bachelor(X);married(X):-man(X),adult(X))).
cl((has_wife(X):-man(X),married(X))).
cl((false:-has_wife(paul))).
cl((man(paul):-true)).
cl((adult(paul):-true)).
%%% auxiliary predicates
disj_append(A,B,C):-
( A=false -> B=C
; A=(A1;A2) -> C=(A1;C2),disj_append(A2,B,C2)
; otherwise -> C=(A;B)
).
conj_append(A,B,C):-
( A=true -> B=C
; A=(A1,A2) -> C=(A1,C2),conj_append(A2,B,C2)
; otherwise -> C=(A,B)
).
conj_remove_one(X,X,true):- % single-element conjunction
not(X=true),not(X=(_,_)).
conj_remove_one(X,(X,Ys),Ys).
conj_remove_one(X,(Y,Ys),(Y,Zs)):-
conj_remove_one(X,Ys,Zs).
/** <examples>
?- refute_bf((false:-bachelor(X))).
*/
cl((bachelor(X);married(X):-man(X),adult(X))). cl((has_wife(X):-man(X),married(X))). %cl((false:-has_wife(paul))). cl((man(paul):-true)). cl((adult(paul):-true)). model(M0,M):- is_violated(Head,M0),!, % find instance of violated clause disj_element(L,Head), % select ground literal from the head model([L|M0],M). % and add it to the model model(M,M). % no more violated clauses is_violated(H,M):- cl((H:-B)), satisfied_body(B,M), % this will ground the variables not(satisfied_head(H,M)). satisfied_body(true,_M). % body is a conjunction satisfied_body(A,M):- member(A,M). satisfied_body((A,B),M):- member(A,M), satisfied_body(B,M). satisfied_head(A,M):- % head is a disjunction member(A,M). satisfied_head((A;_B),M):- member(A,M). satisfied_head((_A;B),M):- satisfied_head(B,M). disj_element(X,X):- % single-element disjunction not(X=false),not(X=(_;_)). disj_element(X,(X;_Ys)). disj_element(X,(_Y;Ys)):- disj_element(X,Ys). /** <examples> ?- model([],M). */
cl((append([],Y,Y):-list(Y))). cl((append([X|Xs],Ys,[X|Zs]):-thing(X),append(Xs,Ys,Zs))). cl((list([]):-true)). cl((list([X|Y]):-thing(X),list(Y))). cl((thing(a):-true)). cl((thing(b):-true)). %cl((thing(c):-true)). model_d(0,M,M). model_d(D,M0,M):- D>0,D1 is D-1, findall(H,is_violated(H,M0),Heads), satisfy_clauses(Heads,M0,M1), model_d(D1,M1,M). satisfy_clauses([],M,M). satisfy_clauses([H|Hs],M0,M):- disj_element(L,H), satisfy_clauses(Hs,[L|M0],M). is_violated(H,M):- cl((H:-B)), satisfied_body(B,M), % this will ground the variables not(satisfied_head(H,M)). satisfied_body(true,_M). % body is a conjunction satisfied_body(A,M):- member(A,M). satisfied_body((A,B),M):- member(A,M), satisfied_body(B,M). satisfied_head(A,M):- % head is a disjunction member(A,M). satisfied_head((A;_B),M):- member(A,M). satisfied_head((_A;B),M):- satisfied_head(B,M). disj_element(X,X):- % single-element disjunction not(X=false),not(X=(_;_)). disj_element(X,(X;_Ys)). disj_element(X,(_Y;Ys)):- disj_element(X,Ys). /** <examples> ?- model_d(4,[],M). */
board_size(9). % odd number, at least 3
eval_pos(Pos,Value):-
%% uncomment exactly one of the following lines
%bLeftOfw(Pos,Value).
outOfPlace(Pos,1,Value).
/*
* Moves are represented as triples m(From,To,Cost).
* Agenda items are represented as pairs v(Value,[Move|Moves])
* where Value is the heuristic value of Move obtained by ?-eval_move(Move,Value).
*/
% tiles(M,C) <- moves M lead to a goal position at cost C
% (best-first search strategy)
tiles(Moves,Cost):-
start_pos(Start),
eval_pos(Start,Value),
tiles_a([v(Value,[m(noparent,Start,0)])],Moves,[],_Visited),
get_cost(Moves,0,Cost).
% write solution to screen
tiles(Cost):-
tiles(Moves,Cost),
writeln('# Final list of moves #'),
reverse(Moves,MovesR),
write_moves(MovesR,0).
% tiles_a(A,M,V0,V) <- goal position can be reached from one of the
% positions on A with moves M (best-first)
% (V is list of visited nodes, V0 is accumulator)
tiles_a([v(_V,[LastMove|Moves])|_Rest],[LastMove|Moves],Visited,Visited):-
eval_move(LastMove,0). % reached our goal
tiles_a([v(_V,[LastMove|_])|Rest],Moves,Visited0,Visited):-
eval_move(LastMove,0),!, % to get alternate solutions
tiles_a(Rest,Moves,Visited0,Visited).
tiles_a(Agenda,Moves,Visited0,Visited):-
% writeln('### current agenda (reversed) ###'),reverse(Agenda,AgendaR),write_agenda(AgendaR),readln(_),
%% uncomment the previous line to see agenda at each iteration
Agenda=[v(_V,[LastMove|Ms])|Rest],
( setof(v(Value,[NextMove,LastMove|Ms]),
candidate(LastMove,NextMove,Value,Rest,Visited0),
Children) -> new_agenda(Children,Rest,NewAgenda) % best-first
; otherwise -> NewAgenda=Rest % candidate/5 failed
),tiles_a(NewAgenda,Moves,[LastMove|Visited0],Visited).
candidate(LastMove,NextMove,Value,Agenda,Visited):-
last2next_move(LastMove,NextMove),
NextMove=m(_Pos,NewPos,_Cost),
eval_move(NextMove,Value),
not((member(v(_,[m(_,NewPos,_)|_]),Agenda))), % NewPos already on Agenda
not((member(m(_,NewPos,_),Visited))). % NewPos already visited
% The last two lines implement aggressive pruning as only NewPos matters,
% not the position Pos from which it is reached.
eval_move(m(_P,Pos,_C),Value):-
eval_pos(Pos,Value).
last2next_move(m(_OldPos,Pos,_OldCost),m(Pos,NewPos,Cost)):-
last2next_pos(Pos,NewPos,Cost).
% merge children and agenda
new_agenda([],Agenda,Agenda).
new_agenda([C|Cs],[],[C|Cs]).
new_agenda([v(V1,Moves1)|Rest1],[v(V2,Moves2)|Rest2],NewAgenda):-
( V2>V1 -> new_agenda(Rest1,[v(V2,Moves2)|Rest2],Rest3),NewAgenda=[v(V1,Moves1)|Rest3]
; otherwise -> new_agenda([v(V1,Moves1)|Rest1],Rest2,Rest3),NewAgenda=[v(V2,Moves2)|Rest3]
).
get_cost([],C,C).
get_cost([m(_From,_To,C)|Moves],Cost0,Cost):-
Cost1 is Cost0+C,
get_cost(Moves,Cost1,Cost).
write_agenda([]):-
writeln('-------------------').
write_agenda([P|Ps]):-
write_agenda_item(P),nl,
write_agenda(Ps).
write_agenda_item(v(Value,[m(_P,Pos,_C)|_Rest])):-
write_pos(Pos),
write(' : '),write(Value).
write_moves([],_):-
writeln('-------------------').
write_moves([m(_P,Pos,C)|Moves],Cost):-
eval_pos(Pos,Value),
Cost1 is Cost+C,
write_pos(Pos),
format(' : ~|~` t~d~2+ :~|~` t~d~3+~n', [Value,Cost1]),
write_moves(Moves,Cost1).
%%% board predicates
start_pos(Start):-
board_size(N),
start_pos(Start,N).
start_pos(Start,N):-
N1 is (N-1)/2,
start_lr(Left,N1,b),
start_lr(Right,N1,w),
append(Left,[e|Right],Start).
start_lr(LR,N,BW):-
length(LR,N),
start_lr(LR,BW).
start_lr([],_).
start_lr([BW|LR],BW):-
start_lr(LR,BW).
last2next_pos(Pos,NewPos,Cost):-
get_tile(Pos,Ne,e),get_tile(Pos,Nbw,BW),not(BW=e),
Diff is abs(Ne-Nbw),
Diff<4,
replace(Pos,Ne,BW,Pos1),
replace(Pos1,Nbw,e,NewPos),
( Diff=1 -> Cost=1
; otherwise -> Cost is Diff-1 ).
write_pos([]).
write_pos([P|Ps]):-
( P=e -> write('. ')
; P=b -> write('\x25cf'),write(' ')
; P=w -> write('\x25cb'),write(' ')
),write_pos(Ps).
get_tile(Pos,N,S):-
get_tile(Pos,1,N,S).
get_tile([X|_Xs],N,N,X).
get_tile([_X|Xs],N0,N,Y):-
N1 is N0+1,
get_tile(Xs,N1,N,Y).
%%% heuristics
bLeftOfw(Pos,Value):-
findall(b,(get_tile(Pos,Nb,b),get_tile(Pos,Nw,w),Nw>Nb),L),
length(L,Value).
outOfPlace(Pos,Initial,Value):-
append(L,[_Mid|Right],Pos), % generate
length(L,N),length(Right,N), % test
reverse(L,Left), % from low to high penalty
penalise(Left,b,Initial,0,VL),
penalise(Right,w,Initial,0,VR),
Value is VL+VR.
penalise([],_,_,V,V).
penalise([H|T],BW,P,V0,V):-
( H=BW -> V1 is V0+P
; otherwise -> V1=V0
),
P1 is P+1,
penalise(T,BW,P1,V1,V).
%%% auxiliary predicates
% replace(In,Pos,Item,Out) <- list Out is List in with item at Pos replaced with Item
replace([_X|Xs],1,Y,[Y|Xs]).
replace([X|Xs],N,Y,[X|Zs]):-
N>1,N1 is N-1,
replace(Xs,N1,Y,Zs).
/** <examples>
?- tiles(Moves,Cost).
?- tiles(Cost). % prints agenda
*/
path(SS):-
width(W),height(H),empty_grid(W,H,Grid),
setx_hor(5/3,4,Grid),setx_hor(7/6,2,Grid),setx_hor(3/9,4,Grid),
setx_ver(2/5,3,Grid),setx_ver(4/4,3,Grid),setx_ver(7/7,2,Grid),
search(Grid,SS),show_grid(Grid).
width(8). height(10).
entrance(1/1). exit(8/5). %exit(3/5).
/*
* Search predicates
* move/2 enumerates all possible moves, ignoring whether cell is free
* search/2 searches grid with various search strategies
*/
:-use_module(library(lists)).
moves(X/Y,Moves):-
bagof(X1/Y1,move(X/Y,X1/Y1),Moves).
move(X/Y,X/Y1):-
height(H),
H>Y,Y1 is Y+1. % down
move(X/Y,X1/Y):-
width(W),
W>X,X1 is X+1. % right
move(X/Y,X/Y1):-
Y>1,Y1 is Y-1. % up
move(X/Y,X1/Y):-
X>1,X1 is X-1. % left
% for A* search: generates moves with increasing F-value
moves_h(F/G:X/Y,Moves):-
setof(F1/G1:X1/Y1,move_h(F/G:X/Y,F1/G1:X1/Y1),Moves).
move_h(_/G:X/Y,F1/G1:X1/Y1):-
move(X/Y,X1/Y1),
h(X1/Y1,H1),
G1 is G+1, % increase G-value from previous
F1 is G1+H1. % add new H-value
h(X/Y,H):-
exit(XE/YE),
H is abs(XE-X)+abs(YE-Y). % Manhattan distance
search(Grid,SS):-
entrance(X/Y),
( SS=bt -> search_bt(0,X/Y,Grid) % backtracking search
; SS=df -> search_df(0,[X/Y],Grid) % agenda-based depth-first
; SS=bf -> search_bf(0,[X/Y],Grid) % agenda-based breadth-first
; SS=as -> h(X/Y,H),search_as(0,[H/0:X/Y],Grid) % A* search
).
% backtracking search
% only path found is indicated in grid
search_bt(N,X/Y,Grid):-
exit(X/Y),
set(X/Y,Grid,N).
search_bt(N,X/Y,Grid):-
N1 is N+1,
set(X/Y,Grid,N),
move(X/Y,X1/Y1),
search_bt(N1,X1/Y1,Grid).
% agenda-based depth-first search
% grid is used for loop-detection: if set/3 fails, it is either an obstacle
% or we've been there already
search_df(N,[X/Y|_],Grid):-
exit(X/Y),
set(X/Y,Grid,N).
search_df(N,[X/Y|Agenda],Grid):-
( set(X/Y,Grid,N) -> moves(X/Y,Moves),N1 is N+1,
append(Moves,Agenda,NewAgenda)
; otherwise -> NewAgenda=Agenda,N1=N % ignore: can't go there
),search_df(N1,NewAgenda,Grid).
% agenda-based breadth-first search
search_bf(N,[X/Y|_],Grid):-
exit(X/Y),
set(X/Y,Grid,N).
search_bf(N,[X/Y|Agenda],Grid):-
( set(X/Y,Grid,N) -> moves(X/Y,Moves),N1 is N+1,
append(Agenda,Moves,NewAgenda)
; otherwise -> NewAgenda=Agenda,N1=N % ignore: can't go there
),search_bf(N1,NewAgenda,Grid).
% A* search: agenda contains F/G:X/Y with F=G+H evaluation of position X/Y
search_as(N,[_:X/Y|_],Grid):-
exit(X/Y),
set(X/Y,Grid,N).
search_as(N,[F/G:X/Y|Agenda],Grid):-
( set(X/Y,Grid,N) -> moves_h(F/G:X/Y,Moves),N1 is N+1,
merge_h(Moves,Agenda,NewAgenda)
; otherwise -> NewAgenda=Agenda,N1=N % ignore: can't go there
),search_as(N1,NewAgenda,Grid).
merge_h([],Agenda,Agenda).
merge_h(Moves,[],Moves).
merge_h([F/G:X/Y|Moves],[F1/G1:X1/Y1|Agenda],[F/G:X/Y|NewAgenda]):-
F1>F,
merge_h(Moves,[F1/G1:X1/Y1|Agenda],NewAgenda).
merge_h([F/G:X/Y|Moves],[F1/G1:X1/Y1|Agenda],[F1/G1:X1/Y1|NewAgenda]):-
F>=F1,
merge_h([F/G:X/Y|Moves],Agenda,NewAgenda).
/*
* Grid datastructure: list of H rows of length W.
* A variable indicates cell is empty, so it can be
* instantiated once with 'x' to indicate an obstacle
* or with a number to indicate at which search iteration
* it was explored.
*/
empty_grid(W,H,Grid):-
length(Grid,H), % generate a list of variables of length H
empty_rows(W,Grid). % and instantiate each variable to an empty row
empty_rows(_,[]).
empty_rows(W,[Row|Rows]):-
length(Row,W), % generate a list of variables of length W
empty_rows(W,Rows).
get_row(N,Grid,Row):-
nth1(N,Grid,Row).
get_col(_,[],[]).
get_col(N,[Row|Rows],[X|Col]):-
nth1(N,Row,X),
get_col(N,Rows,Col).
% Create horizontal/vertical obstacles at position X/Y with length L
setx_hor(X/Y,L,Grid):-
get_row(Y,Grid,Row),
setx(X,L,Row).
setx_ver(X/Y,L,Grid):-
get_col(X,Grid,Col),
setx(Y,L,Col).
setx(_,0,_).
setx(X,L,Row):-
L>0,L1 is L-1,X1 is X+1,
nth1(X,Row,x),
setx(X1,L1,Row).
% Set cell X/Y to N; fails if cell has been set already
set(X/Y,Grid,N):-
get_row(Y,Grid,Row),
nth1(X,Row,C),
var(C),
C=N.
show_grid(Grid):-
nl,
show_rows(Grid),
nl.
show_rows([]).
show_rows([Row|Rows]):-
show_row(Row),
show_rows(Rows).
show_row([]):-nl.
show_row([H|T]):-
( var(H) -> format('~|~` t~w~3+ ',['.'])
; H=x -> format('~|~` t~w~3+ ',[H])
; otherwise -> format('~|~` t~d~3+ ',[H])
),show_row(T).
/** <examples>
?- member(SS,[df,bf,as,bt]),path(SS).
*/
%% Roman numerals %%
% adapted from https://groups.google.com/forum/#!topic/comp.compilers/g8Qvp-KGbig
roman(N) --> d(N4,4),d(N3,3),d(N2,2),d(N1,1),{N is N4*1000+N3*100+N2*10+N1}.
i(1) --> [i].
i(2) --> [x].
i(3) --> [c].
i(4) --> [m].
v(1) --> [v].
v(2) --> [l].
v(3) --> [d].
d(0,_) --> [].
d(1,N) --> i(N).
d(2,N) --> i(N),i(N).
d(3,N) --> i(N),i(N),i(N).
d(4,N) --> i(N),v(N).
%d(4,N) --> i(N),i(N),i(N),i(N).
d(5,N) --> v(N).
d(6,N) --> v(N),i(N).
d(7,N) --> v(N),i(N),i(N).
d(8,N) --> v(N),i(N),i(N),i(N).
d(9,N) --> i(N),{N1 is N+1},i(N1).
/** <examples>
?- phrase(roman(1984),R).
?- phrase(roman(Y),[m,c,m,l,x,x,x,i,v]).
*/
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% Prolog programs from Section 9.2 of the book %
% SIMPLY LOGICAL: Intelligent reasoning by example %
% (c) Peter A. Flach/John Wiley & Sons, 1994. %
% %
% Predicates: induce_rlgg/2 %
% rlgg/4 %
% %
% NB. This file needs predicates defined in %
% the file 'library'. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%:-consult(library).
%%% 9.2 Bottom-up induction %%%
induce_rlgg(Exs,Clauses):-
writeln('%%% Bottom-up induction %%%'),
writeln('Examples'),
writelns(Exs),
pos_neg(Exs,Poss,Negs),
bg_model(BG),
append(Poss,BG,Model),
induce_rlgg(Poss,Negs,Model,Clauses).
induce_rlgg(Poss,Negs,Model,Clauses):-
covering(Poss,Negs,Model,[],Clauses).
% split positive and negative examples
pos_neg([],[],[]).
pos_neg([+E|Exs],[E|Poss],Negs):-
pos_neg(Exs,Poss,Negs).
pos_neg([-E|Exs],Poss,[E|Negs]):-
pos_neg(Exs,Poss,Negs).
% covering algorithm
covering(Poss,Negs,Model,H0,H):-
construct_hypothesis(Poss,Negs,Model,Hyp),!,
remove_pos(Poss,Model,Hyp,NewPoss),
nl,writeln(' to continue'),
readln(_),nl,nl,
covering(NewPoss,Negs,Model,[Hyp|H0],H).
covering(P,_N,_M,H0,H):-
append(H0,P,H). % add uncovered examples to hypothesis
% remove covered positive examples
remove_pos([],_M,_H,[]).
remove_pos([P|Ps],Model,Hyp,NewP):-
covers_ex(Hyp,P,Model),!,
write('Covered example: '),write(P),nl,
remove_pos(Ps,Model,Hyp,NewP).
remove_pos([P|Ps],Model,Hyp,[P|NewP]):-
remove_pos(Ps,Model,Hyp,NewP).
% extensional coverage, relative to a ground model
covers_ex((Head:-Body),Example,Model):-
try((Head=Example,forall(element(L,Body),element(L,Model)))).
% construct a clause by means of RLGG
construct_hypothesis([E1,E2|_Es],Negs,Model,Clause):-
write('RLGG of '),write(E1),write(' and '),write(E2),write(' is'),
rlgg(E1,E2,Model,Cl),
reduce(Cl,Negs,Model,Clause),!,
nl,portray_clause(Clause),nl.
construct_hypothesis([_E1,E2|Es],Negs,Model,Clause):-
write(' too general'),nl,
construct_hypothesis([E2|Es],Negs,Model,Clause).
% rlgg(E1,E2,M,C) <- C is RLGG of E1 and E2 relative to M
rlgg(E1,E2,M,(H:-B)):-
anti_unify(E1,E2,H,[],S10,[],S20),
varsin(H,V), % determine variables in head of clause
rlgg_bodies(M,M,[],B,S10,_S1,S20,_S2,V).
rlgg_bodies([],_B2,B,B,S1,S1,S2,S2,_V).
rlgg_bodies([L|B1],B2,B0,B,S10,S1,S20,S2,V):-
rlgg_literal(L,B2,B0,B00,S10,S11,S20,S21,V),
rlgg_bodies(B1,B2,B00,B,S11,S1,S21,S2,V).
rlgg_literal(_L1,[],B,B,S1,S1,S2,S2,_V).
rlgg_literal(L1,[L2|B2],B0,B,S10,S1,S20,S2,V):-
same_predicate(L1,L2),
anti_unify(L1,L2,L,S10,S11,S20,S21),
varsin(L,Vars),var_proper_subset(Vars,V), % no new variables in literal
!,rlgg_literal(L1,B2,[L|B0],B,S11,S1,S21,S2,V).
rlgg_literal(L1,[_L2|B2],B0,B,S10,S1,S20,S2,V):-
rlgg_literal(L1,B2,B0,B,S10,S1,S20,S2,V).
:-op(600,xfx,'<-').
anti_unify(Term1,Term2,Term):-
anti_unify(Term1,Term2,Term,[],_S1,[],_S2).
anti_unify(Term1,Term2,Term1,S1,S1,S2,S2):-
Term1 == Term2,!.
anti_unify(Term1,Term2,V,S1,S1,S2,S2):-
subs_lookup(S1,S2,Term1,Term2,V),!.
anti_unify(Term1,Term2,Term,S10,S1,S20,S2):-
nonvar(Term1),nonvar(Term2),
functor(Term1,F,N),functor(Term2,F,N),!,
functor(Term,F,N),
anti_unify_args(N,Term1,Term2,Term,S10,S1,S20,S2).
anti_unify(Term1,Term2,V,S10,[Term1<-V|S10],S20,[Term2<-V|S20]).
anti_unify_args(0,_Term1,_Term2,_Term,S1,S1,S2,S2).
anti_unify_args(N,Term1,Term2,Term,S10,S1,S20,S2):-
N>0,N1 is N-1,
arg(N,Term1,Arg1),
arg(N,Term2,Arg2),
arg(N,Term,Arg),
anti_unify(Arg1,Arg2,Arg,S10,S11,S20,S21),
anti_unify_args(N1,Term1,Term2,Term,S11,S1,S21,S2).
subs_lookup([T1<-V|_Subs1],[T2<-V|_Subs2],Term1,Term2,V):-
T1 == Term1,
T2 == Term2,!.
subs_lookup([_S1|Subs1],[_S2|Subs2],Term1,Term2,V):-
subs_lookup(Subs1,Subs2,Term1,Term2,V).
% remove redundant literals
reduce((H:-B0),Negs,M,(H:-B)):-
setof0(L,(element(L,B0),not(var_element(L,M))),B1),
reduce_negs(H,B1,[],B,Negs,M).
% reduce_negs(H,B1,B0,B,N,M) <- B is a subsequence of B1
% such that H:-B does not
% cover elements of N
reduce_negs(H,[_L|B0],In,B,Negs,M):-
append(In,B0,Body),
not(covers_neg((H:-Body),Negs,M,_N)),!,
reduce_negs(H,B0,In,B,Negs,M).
reduce_negs(H,[L|B0],In,B,Negs,M):-
reduce_negs(H,B0,[L|In],B,Negs,M).
reduce_negs(H,[],Body,Body,Negs,M):-
not(covers_neg((H:-Body),Negs,M,_N)).
covers_neg(Clause,Negs,Model,N):-
element(N,Negs),
covers_ex(Clause,N,Model).
%%% From library %%%
%%% Lists and sets
% element(X,Ys) <- X is an element of the list Ys
element(X,[X|_Ys]).
element(X,[_Y|Ys]):-
element(X,Ys).
var_element(X,[Y|_Ys]):-
X == Y. % syntactic identity
var_element(X,[_Y|Ys]):-
var_element(X,Ys).
var_remove_one(X,[Y|Ys],Ys):-
X == Y. % syntactic identity
var_remove_one(X,[Y|Ys],[Y|Zs]):-
var_remove_one(X,Ys,Zs).
var_proper_subset([],Ys):-
Ys \= [].
var_proper_subset([X|Xs],Ys):-
var_remove_one(X,Ys,Zs),
var_proper_subset(Xs,Zs).
% try(Goal) <- Goal succeeds, but variables are not instantiated
try(Goal):-
not(not(Goal)).
%%% Various.
% variant of setof/3 which succeeds with the empty list
% if no solutions can be found
setof0(X,G,L):-
setof(X,G,L),!.
setof0(_X,_G,[]).
% same_predicate(L1,L2) <- literals L1 and L2 have
% the same predicate and arity
same_predicate(L1,L2):-
functor(L1,P,N),functor(L2,P,N).
varsin(Term,Vars):-
varsin(Term,[],V),
sort(V,Vars).
varsin(V,Vars,[V|Vars]):-
var(V),!.
varsin(Term,V0,V):-
functor(Term,_,N),
varsin_args(N,Term,V0,V).
varsin_args(0,_,Vars,Vars).
varsin_args(N,Term,V0,V):-
N>0, N1 is N-1,
arg(N,Term,ArgN),
varsin(ArgN,V0,V1),
varsin_args(N1,Term,V1,V).
%%% For lectures
writelns(X):-
( X=[] -> nl
; X=[H|T] -> writelns(H),writelns(T)
; otherwise -> write(X),nl
).
%%% Queries %%%
%%%%%%%%%%%%%%%%%% element/2 %%%%%%%%%%%%%%%%%%%%%%%%
% bg_model([]).
query1(Clauses):-
induce_rlgg([+element(b,[b]),
+element(2,[2,3]),
+element(3,[1,2,3]),
+element(b,[a,b]),
+element(3,[2,3]),
+element(3,[3]),
-element(3,[a,b]),
-element(a,[])
],Clauses).
%%%%%%%%%%%%%%%%%% append/3 %%%%%%%%%%%%%%%%%%%%%%%
% bg_model([]).
query2(Clauses):-
induce_rlgg([+append([1,2],[3,4],[1,2,3,4]),
+append([a],[],[a]),
+append([],[],[]),
+append([],[1,2,3],[1,2,3]),
+append([2],[3,4],[2,3,4]),
+append([],[3,4],[3,4]),
-append([a],[b],[b]),
-append([c],[b],[c,a]),
-append([1,2],[],[1,3])
],Clauses).
%%%%%%%%%%%%%%%%%% num/2 %%%%%%%%%%%%%%%%%%%%%%%
bg_model([num(1,one),
num(2,two),
num(3,three),
num(4,four),
num(5,five)
]).
query3(Clauses):-
induce_rlgg([+listnum([],[]),
+listnum([2,three,4],[two,3,four]),
+listnum([4],[four]),
+listnum([three,4],[3,four]),
+listnum([two],[2]),
-listnum([1,4],[1,four]),
-listnum([2,three,4],[two]),
-listnum([five],[5,5])
],Clauses).
%%%%%%%%%%%%%%%%%% names/2 %%%%%%%%%%%%%%%%%%%%%%%
/*
bg_model([person(mick,jagger),
person(david,bowie),
person(tina,turner),
person(johann,sebastian),
person(ludwig,van)
]).
*/
query4(Clauses):-
induce_rlgg([+names([],[]),
+names([david,turner,johann],[p(david,bowie),p(tina,turner),p(johann,sebastian)]),
+names([johann],[p(johann,sebastian)]),
+names([turner,johann],[p(tina,turner),p(johann,sebastian)]),
+names([bowie],[p(david,bowie)]),
-names([mick,johann],[p(mick,mick),p(johann,sebastian)]),
-names([david,turner,johann],[p(david,bowie)]),
-names([van],[p(ludwig,van),p(ludwig,van)])
],Clauses).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% Prolog programs from Section 9.3 of the book %
% SIMPLY LOGICAL: Intelligent reasoning by example %
% (c) Peter A. Flach/John Wiley & Sons, 1994. %
% %
% Predicates: induce_spec/2 %
% %
% NB. This file needs predicates defined in %
% the file 'library'. %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:-consult(library).
%%% 9.3 Top-down induction %%%
induce_spec(Examples,Clauses):-
writeln('%%% Top-down induction %%%'),
writeln('Examples'),
writelns(Examples),
process_examples([],[],Examples,Clauses).
% process the examples
process_examples(Clauses,Done,[],Clauses).
process_examples(Cls1,Done,[Ex|Exs],Clauses):-
process_example(Cls1,Done,Ex,Cls2),
process_examples(Cls2,[Ex|Done],Exs,Clauses).
% process one example
process_example(Clauses,Done,+Example,Clauses):-
covers(Clauses,Example).
process_example(Cls,Done,+Example,Clauses):-
not covers(Cls,Example),
generalise(Cls,Done,Example,Clauses).
process_example(Cls,Done,-Example,Clauses):-
covers(Cls,Example),
specialise(Cls,Done,Example,Clauses).
process_example(Clauses,Done,-Example,Clauses):-
not covers(Clauses,Example).
% covers(Clauses,Ex) <- Ex can be proved from Clauses and
% background theory in max. 10 steps
covers(Clauses,Example):-
prove_d(10,Clauses,Example).
prove_d(D,Cls,true):-!.
prove_d(D,Cls,(A,B)):-!,
prove_d(D,Cls,A),
prove_d(D,Cls,B).
prove_d(D,Cls,A):-
D>0,D1 is D-1,
copy_element((A:-B),Cls), % make copy of clause
prove_d(D1,Cls,B).
prove_d(D,Cls,A):-
prove_bg(A).
prove_bg(true):-!.
prove_bg((A,B)):-!,
prove_bg(A),
prove_bg(B).
prove_bg(A):-
bg((A:-B)),
prove_bg(B).
% Specialisation by removing a refuted clause
specialise(Cls,Done,Example,Clauses):-
false_clause(Cls,Done,Example,C),
remove_one(C,Cls,Cls1),
write(' ...refuted: '),write(C),nl,nl,
writeln(' to continue'),readln(_),
process_examples(Cls1,[],[-Example|Done],Clauses).
% false_clause(Cs,E,E,C) <- C is a false clause in the proof of E (or ok)
false_clause(Cls,Exs,true,ok):-!.
false_clause(Cls,Exs,(A,B),X):-!,
false_clause(Cls,Exs,A,Xa),
( Xa = ok -> false_clause(Cls,Exs,B,X)
; otherwise -> X = Xa
).
false_clause(Cls,Exs,E,ok):-
element(+E,Exs),!.
false_clause(Cls,Exs,A,ok):-
bg((A:-B)),!.
false_clause(Cls,Exs,A,X):-
copy_element((A:-B),Cls),
false_clause(Cls,Exs,B,Xb),
( Xb \= ok -> X = Xb
; otherwise -> X = (A:-B)
).
% Generalisation by adding a covering clause
generalise(Cls,Done,Example,Clauses):-
write('Generalising example: '),write(Example),nl,
search_clause(Done,Example,Cl),
writeln('Found clause: '),portray_clause(Cl),nl,
writeln(' to continue'),readln(_),
process_examples([Cl|Cls],[],[+Example|Done],Clauses).
% search_clause(Exs,E,C) <- C is a clause covering E and
% not covering negative examples
% (iterative deepening search)
search_clause(Exs,Example,Clause):-
literal(Head,Vars),
try((Head=Example)),
search_clause(3,a((Head:-true),Vars),Exs,Example,Clause).
search_clause(D,Current,Exs,Example,Clause):-
write(D),write('..'),
search_clause_d(D,Current,Exs,Example,Clause),!.
search_clause(D,Current,Exs,Example,Clause):-
D1 is D+1,
!,search_clause(D1,Current,Exs,Example,Clause).
search_clause_d(D,a(Clause,Vars),Exs,Example,Clause):-
covers_ex(Clause,Example,Exs), % goal
not((element(-N,Exs),covers_ex(Clause,N,Exs))),!.
search_clause_d(D,Current,Exs,Example,Clause):-
D>0,D1 is D-1,
specialise_clause(Current,Spec),
search_clause_d(D1,Spec,Exs,Example,Clause).
% Extensional coverage
covers_ex((Head:-Body),Example,Exs):-
try((Head=Example,covers_ex(Body,Exs))).
covers_ex(true,Exs):-!.
covers_ex((A,B),Exs):-!,
covers_ex(A,Exs),
covers_ex(B,Exs).
covers_ex(A,Exs):-
element(+A,Exs).
covers_ex(A,Exs):-
prove_bg(A).
% specialise_clause(C,S) <- S is a minimal specialisation
% of C under theta-subsumption
specialise_clause(Current,Spec):-
add_literal(Current,Spec).
specialise_clause(Current,Spec):-
apply_subs(Current,Spec).
add_literal(a((H:-true),Vars),a((H:-L),Vars)):-!,
literal(L,LVars),
proper_subset(LVars,Vars).
add_literal(a((H:-B),Vars),a((H:-L,B),Vars)):-
literal(L,LVars),
proper_subset(LVars,Vars).
apply_subs(a(Clause,Vars),a(Spec,SVars)):-
copy_term(a(Clause,Vars),a(Spec,Vs)),
apply_subs1(Vs,SVars).
apply_subs1(Vars,SVars):-
unify_two(Vars,SVars).
apply_subs1(Vars,SVars):-
subs_term(Vars,SVars).
unify_two([X|Vars],Vars):-
element(Y,Vars),
X=Y.
unify_two([X|Vars],[X|SVars]):-
unify_two(Vars,SVars).
subs_term(Vars,SVars):-
remove_one(X,Vars,Vs),
term(Term,TVars),
X=Term,
append(Vs,TVars,SVars).
%%% Queries %%%
term(list([]),[]).
term(list([X|Y]),[item(X),list(Y)]).
%%%%%%%%%%%%%%%%%% element/2 %%%%%%%%%%%%%%%%%%%%%%%%
/*
literal(element(X,Y),[item(X),list(Y)]).
bg(true).
*/
query1(Clauses):-
induce_spec([+element(a,[a,b]),
-element(x,[a,b]),
+element(b,[b]),
+element(b,[a,b])
],Clauses).
%%%%%%%%%%%%%%%%%% append/3 %%%%%%%%%%%%%%%%%%%%%%%
/*
literal(append(X,Y,Z),[list(X),list(Y),list(Z)]).
bg(true).
*/
query2(Clauses):-
induce_spec([+append([],[b,c],[b,c]),
-append([],[a,b],[c,d]),
-append([a,b],[c,d],[c,d]),
-append([a],[b,c],[d,b,c]),
-append([a],[b,c],[a,d,e]),
+append([a],[b,c],[a,b,c])
],Clauses).
%%%%%%%%%%%%%%%%%% listnum/2 %%%%%%%%%%%%%%%%%%%%%%%
literal(listnum(X,Y),[list(X),list(Y)]).
literal(num(X,Y),[item(X),item(Y)]).
bg((num(1,one):-true)).
bg((num(2,two):-true)).
bg((num(3,three):-true)).
bg((num(4,four):-true)).
bg((num(5,five):-true)).
query3(Clauses):-
induce_spec([+listnum([],[]),
-listnum([one],[one]),
-listnum([1,two],[one,two]),
+listnum([1],[one]),
-listnum([five,two],[5,two]),
+listnum([five],[5])
],Clauses).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%