3
7
8solve(G,N,P) <-
9 solve(G,[G],N,P).
10
11solve(G,_,_,init) <-
12 solved(G).
13
14solve(G,AS,NAs,do(A,Pl)) <-
15 NAs > 0 &
16 satisfiable(G) &
17 useful(G,A) &
18 wp(G,A,G1) &
19 ~ subgoal_loop(G1,AS) &
20 NA1 is NAs-1 &
21 solve(G1,[G1|AS],NA1,Pl).
22
25subgoal_loop(G1,AS) <-
26 grnd(G1)& member(An,AS)& subset(An,G1).
27
29solved([]).
30solved([G|R]) <-
31 holds(G,init) &
32 solved(R).
33
36satisfiable(G) <-
37 ~ unsatisfiable(G).
38
41useful([S|R],A) <-
42 holds(S,init) &
43 useful(R,A).
44useful([S|_],A) <-
45 achieves(A,S).
46useful([S|R],A) <-
47 ~ holds(S,init) &
48 useful(R,A).
49
52useful(G,A) <-
53 member(S,G) &
54 member(S,[handempty])& 55 holds(S,init) &
56 achieves(S,A).
57
60wp([],A,G1) <-
61 preconditions(A,G) &
62 filter_derived(G,[],G1).
63wp([S|R],A,G1) <-
64 wp(R,A,G0) &
65 regress(S,A,G0,G1).
66
69regress(S,A,G,G) <-
70 achieves(A,S).
71regress(S,A,G,G1) <-
72 primitive(S) &
73 ~ achieves(A,S) &
74 ~ deletes(A,S) &
75 insert(S,G,G1).
76
77filter_derived([],L,L).
78filter_derived([G|R],L,[G|L1]) <-
79 primitive(G) &
80 filter_derived(R,L,L1).
81filter_derived([A \= B | R],L,L1) <-
82 dif(A,B) &
83 filter_derived(R,L,L1).
84filter_derived([G|R],L0,L2) <-
85 (G <- B) &
86 filter_derived(R,L0,L1) &
87 filter_derived(B,L1,L2).
88
89regress_all([],_,G,G).
90regress_all([S|R],A,G0,G2) <-
91 regress(S,A,G0,G1) &
92 regress_all(R,A,G1,G2).
93
95
97member(X,[X|_]).
98member(X,[_|L]) <-
99 member(X,L).
100
101notin(_,[]).
102notin(A,[B|C]) <-
103 dif(A,B) &
104 notin(A,C).
105
107subset([],_).
108subset([A|B],L) <-
109 member(A,L) &
110 subset(B,L).
111
114insert(A,[],[A]).
115insert(A,[B|L],[A|L]) <- A==B.
116insert(A,[B|L],[B|R]) <-
117 ~ A == B &
118 insert(A,L,R).
119grnd(G) <-
120 numbervars(G,0,_).
121
124unsatisfiable(L) <-
125 member(sitting_at(X1,Y1),L) &
126 member(sitting_at(X2,Y2),L) &
127 X1 == X2 &
128 ~ (Y1=Y2).
129unsatisfiable(L) <-
130 member(sitting_at(X1,_),L) &
131 member(carrying(_,Y2),L) &
132 X1 == Y2.
133unsatisfiable(L) <-
134 member(carrying(X1,Y1),L) &
135 member(carrying(X2,Y2),L) &
136 Y1 == Y2 &
137 (X1\=X2).
138