%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%% dnf example %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Convert a propositional formula into disjunctive normal form. % There are 15 goals ?- go1 to ?- go 15. % The goal ?- go5 is the most substantial. % literal(z0). literal(z1). literal(z2). literal(z3). literal(z4). literal(z5). literal(z6). literal(z7). literal(z8). literal(z9). literal(n(X)) :- literal(X). norm(X, X) :- literal(X). norm(o(X, Y), o(X, Y)) :- literal(X), literal(Y). norm(a(X, Y), a(X, Y)) :- literal(X), literal(Y). norm(o(X, Y), o(X1, Y)) :- literal(Y), norm(X, X1). norm(o(X, o(Y, Z)), W) :- norm(o(o(X, Y), Z), W). norm(o(X, a(Y1, Y2)), o(X1, Y12)) :- norm(X, X1), norm(a(Y1, Y2), Y12). norm(a(X, Y), a(X1, Y)) :- literal(Y), norm(X, X1). norm(a(X, a(Y, Z)), W) :- norm(a(a(X, Y), Z), W). norm(a(X, o(Y1, Y2)), a(X1, Y12)) :- norm(X, X1), norm(o(Y1, Y2), Y12). dnf(X, X) :- literal(X). dnf(o(X, Y), o(X, Y)) :- literal(X), literal(Y). dnf(a(X, Y), a(X, Y)) :- literal(X), literal(Y). dnf(n(n(X)), W) :- dnf(X, W). dnf(n(o(X, Y)), W) :- dnf(a(n(X), n(Y)), W). dnf(n(a(X, Y)), W) :- dnf(o(n(X), n(Y)), W). dnf(o(X, Y), W) :- dnf(X, X1), dnf(Y, Y1), norm(o(X1, Y1), W). dnf(a(X, Y), a(a(X1, X2), Y)) :- literal(Y), dnf(X, a(X1, X2)). dnf(a(X, Y), a(a(Y1, Y2), X)) :- literal(X), dnf(Y, a(Y1, Y2)). dnf(a(X, Y), W) :- dnf(X, a(X1, X2)), dnf(Y, a(Y1, Y2)), norm(a(a(X1, X2), a(Y1, Y2)), W). dnf(a(X, Y), W) :- dnf(X, o(X1, X2)), dnf(Y, Y1), dnf(o(a(X1, Y1), a(X2, Y1)), W). dnf(a(X, Y), W) :- dnf(X, X1), dnf(Y, o(Y1, Y2)), dnf(o(a(X1, Y1), a(X1, Y2)), W). % ?- dnf(?, *). ?- dnf(*, ?). %%% 32 rules (10 facts + 22 non-facts) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Imperative Language Operational Semantics %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% prog_var(x). prog_var(y). prog_var(z). diff_var(x, y). diff_var(x, z). diff_var(y, x). diff_var(y, z). diff_var(z, x). diff_var(z, y). prog_const(a). prog_const(b). prog_const(c). diff_const(a, b). diff_const(a, c). diff_const(b, a). diff_const(b, c). diff_const(c, a). diff_const(c, b). lookup_var(Var, [[Var, E] | _Env], E). lookup_var(Var, [[Var2, _E2] | Env], E) :- diff_var(Var, Var2), lookup_var(Var, Env, E). change_env(Var, E, [[Var, _E2] | Env], [[Var, E] | Env]). change_env(Var, E, [], [[Var, E]]). change_env(Var, E, [[Var1, E1] | Env1], [[Var1, E1] | Env2]) :- diff_var(Var, Var1), change_env(Var, E, Env1, Env2). eval_exp(C, _Env, C) :- prog_const(C). eval_exp([], _Env, []). eval_exp([E | F], Env, [E1 | F1]) :- eval_exp(E, Env, E1), eval_exp(F, Env, F1). eval_exp(car(E), Env, F1) :- eval_exp(E, Env, [F1 | _F2]). eval_exp(cdr(E), Env, F2) :- eval_exp(E, Env, [_F1 | F2]). eval_exp(Var, Env, E) :- prog_var(Var), lookup_var(Var, Env, E). not_equal_val(C1, C2) :- diff_const(C1, C2). not_equal_val(C, []) :- prog_const(C). not_equal_val([], C) :- prog_const(C). not_equal_val(C, [_E | _F]) :- prog_const(C). not_equal_val([_E | _F], C) :- prog_const(C). not_equal_val([], [_E | _F]). not_equal_val([_E | _F], []). eval_cond(match_cons(E), Env) :- eval_exp(E, Env, [_E1 | _E2]). eval_cond(eq(E1, E2), Env) :- eval_exp(E1, Env, F), eval_exp(E2, Env, F). eval_cond(and(C1, C2), Env) :- eval_cond(C1, Env), eval_cond(C2, Env). eval_cond(or(C1, _C2), Env) :- eval_cond(C1, Env). eval_cond(or(_C1, C2), Env) :- eval_cond(C2, Env). eval_cond(not(C), Env) :- not_eval_cond(C, Env). not_eval_cond(match_cons(E), Env) :- eval_exp(E, Env, F), not_equal_val(F, [_F1, _F2]). not_eval_cond(eq(E1,E2), Env) :- eval_exp(E1, Env, F1), eval_exp(E2, Env, F2), not_equal_val(F1, F2). not_eval_cond(and(C1, _C2), Env) :- not_eval_cond(C1, Env). not_eval_cond(and(_C1, C2), Env) :- not_eval_cond(C2, Env). not_eval_cond(or(C1, C2), Env) :- not_eval_cond(C1, Env), not_eval_cond(C2, Env). not_eval_cond(not(C), Env) :- eval_cond(C, Env). eval_stat(assign(Var, E), Env1, Env2) :- prog_var(Var), eval_exp(E, Env1, F), change_env(Var, F, Env1, Env2). eval_stat(if(C, S1, _S2), Env1, Env2) :- eval_cond(C, Env1), eval_stat(S1, Env1, Env2). eval_stat(if(C, _S1, S2), Env1, Env2) :- not_eval_cond(C, Env1), eval_stat(S2, Env1, Env2). eval_stat(while(C, S), Env1, Env2) :- eval_cond(C, Env1), eval_stat(S, Env1, Env1a), eval_stat(while(C, S), Env1a, Env2). eval_stat(while(C, _S), Env, Env) :- not_eval_cond(C, Env). eval_stat(sq(S1, S2), Env1, Env2) :- eval_stat(S1, Env1, Env1a), eval_stat(S2, Env1a, Env2). eval_stat(nop, Env, Env). ?- eval_stat(*, [], ?). %% other sample goals %% ?- eval_stat(nop, [], Env). %% ?- eval_stat(sq(assign(x, [a,b]), assign(y, car(x))), [], Env). %% ?- eval_stat(while(not(eq(x, [])), nop), [[x, []]], Env). %% ?- eval_stat(sq(assign(x, [a,b,a]), %% sq(assign(y, car(x)), %% assign(x, cdr(x)))), %% [], Env). %% ?- eval_stat(while(not(eq(x, [])), %% assign(x, cdr(x))), %% [[x,[a,b,c]]], Env). %% ?- eval_stat(sq(assign(x, [a,b,a]), %% while(not(eq(x, [])), %% sq(assign(y, car(x)), %% assign(x, cdr(x))))), %% [], Env). %% %% % 55 rules (25 facts+ 30 non-facts) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%% nrev example %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% app([], L, L). app([H | L1], L2, [H | L]) :- app(L1, L2, L). rev([], []). rev([H | L1], L) :- rev(L1, L2), app(L2, [H], L). % ?- rev(?, *). ?- rev(*, ?). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%% numbers example %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Frank and Tim's binary numbers example % numbers represented as o(s(o(s(empty)))) for 1010 % does set constraint analyser find that standard form is preserved? std1(s(empty)). std1(s(X)) :- std1(X). std1(o(X)) :- std1(X). std(empty). std(X) :- std1(X). succ(empty, s(empty)). succ(o(X), s(X)). succ(s(X), o(Y)) :- succ(X, Y). add(empty, X, X). add(X, empty, X). add(o(X), o(Y), o(Z)) :- add(X, Y, Z). add(o(X), s(Y), s(Z)) :- add(X, Y, Z). add(s(X), o(Y), s(Z)) :- add(X, Y, Z). add(s(X), s(Y), ZZ) :- add(X, Y, Z), succ(s(Z), ZZ). test(X, Y, Z) :- std(X), std(Y), add(X, Y, Z). ?- test(*, *, *). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%% zebra example %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% zebra(Zebraowner,Drinkswater) :- houses(s(s(s(s(s(zero))))), List), member(house( red, englishman, _1, _2, _3) ,List), member(house( _4, spaniard, dog, _5, _6) ,List), member(house(green, _7, _8, coffee, _9) ,List), member(house( _10, ukrainian, _11, tea, _12) ,List), sublist(cons(house(ivory, _13, _14, _15, _16) , cons(house(green, _17, _18, _19, _20), nil)),List), member(house( _21, _22,snail, _23,old_gold),List), member(house(yellow, _24, _25, _26, kools),List), eq(cons(H1,cons(H2,cons( house( _27, _28, _29, milk, _30), cons(H4,cons(H5,nil))))), List), eq(cons(house( _31, norwegian, _32, _33, _34),Hrest), List), nextto(house( _35, _36, _37, _38,chesterfield), house( _39, _40, fox, _41, _42),List), nextto(house( _43, _44, _45, _46, kools), house( _47, _48,horse, _49, _50),List), member(house( _51, _52, _53, orange,lucky_strike),List), member(house( _54, japanese, _55, _56,parliaments),List), nextto(house( _57, norwegian, _58, _59, _60), house( blue, _61, _62, _63, _64),List), member(house( _65, Drinkswater, _66, water, _67),List), member(house( _68, Zebraowner,zebra, _69, _70),List). eq(X, X). houses(zero, nil). houses(s(N), cons(house(Color,Nat,Pet,Drink,Cig), List)) :- houses(N, List). member(X, cons(X,R)). member(X, cons(Y,R)) :- member(X, R). sublist(S, L) :- append(S, S2, L). sublist(S, cons(H,T)) :- sublist(S, T). append(nil, L, L). append(cons(X,R), Y, cons(X,T)) :- append(R, Y, T). nextto(H1, H2, L) :- sublist(cons(H1, cons(H2, nil)), L). nextto(H1, H2, L) :- sublist(cons(H2, cons(H1, nil)), L). ?- zebra(*, ?). % ?- zebra(?, ?). % Answer: % Zebraowner = japanese, Drinkwater = norwegian