WARNING: more substantial motivations and explanations than what is sketched below would be necessary in an actual exam answer. Whenever you are uncertain whether you have to explain something or not there is a very simple solution: explain it, and do not leave anything to chance. ######## Exercise 1: 1a: no. 1b: yes. 1c: no. 1d: no. Try the following queries in SWI-Prolog: unify_with_occurs_check(p(f(X,Y),Y), p(f(V,g(V)),f(Z))). false. unify_with_occurs_check([f(Y,Z),Z|Y], [f(X, g(X)), g(V ), a, b]). Y = X, X = V, V = [a, b], Z = g([a, b]). unify_with_occurs_check(p(f(X,g(a)),b,X,f(Y,Y )), p(V,Z,g(Z),V)). false. unify_with_occurs_check(p(f(X),X,f(Y ),f(Y )), p(Z,g(V ),f(Z),V)). false. (Due to occurs check). ######## Exercise 2: Note that is_graph(graph([], [])) and is_graph(graph([a,b], [edge(a,b), edge(b,a)])) should hold, but is_graph(graph([a,b], [edge(0,1),...]), or is_graph(graph([a,a,b], ...)), ... should NOT hold. Program for 2a: is_graph(graph(V, E)) :- no_duplicates(V), no_duplicates(E), edge_set(V, E). no_duplicates([]). no_duplicates([X|Xs]) :- %Recall that we are allowed to use nonmember/2. nonmember(X, Xs), no_duplicates(Xs). edge_set(_, []). edge_set(V, [edge(X,Y)|Es]) :- member(X, V), member(Y, V), edge_set(V, Es). Program for 2b: %The crucial observation is that one can easily define an edge checking predicate. is_edge(graph(_V,E), X, Y) :- member(edge(X,Y), E). %Then the path predicate is not harder to write than usual (see lab 1). path(G, X, Y) :- is_edge(G, X, Y). path(G, X, Z) :- is_edge(G, X, Y), path(G, Y, Z). %A simple solution is possible: no need for recursion. three_cycle(G) :- is_edge(G, X, Y), is_edge(G, Y, Z), is_edge(G, Z, X), dif(X,Y), dif(Y,Z), dif(X,Z). ######## Exercise 3 Program for 3a: %This definition is not needed in the answer: it is just an example definition which can be used to test the code. pre(X, Y) :- X @< Y. %Since pre/2 is a strict ordering it is useful to define a weaker ordering which allows the two terms to be equal. pre_or_eq(X, Y) :- X @< Y. pre_or_eq(X, X). %Using pre_or_eq/2 we can then easily define max/2 via standard recursive problem solving. Ok for full credit for this subtask. max([X], X). max([X|Xs], X) :- max(Xs, Y), pre(Y,X). max([X|Xs], Y) :- max(Xs, Y), pre_or_eq(X,Y). %But there is a better solution where we introduce an auxillary predicate largest/3: largest(X, X, X). largest(X, Y, Y) :- pre(X, Y). largest(X, Y, X) :- pre(Y, X). max1([X], X). max1([X|Xs], M) :- max1(Xs, Y), largest(X,Y,M). Program for 3b: %Simple but inefficient version of remove maximal: rmv([X], X, []). rmv([X|Xs], X, Xs) :- rmv(Xs, Max, _Xs), pre_or_eq(Max, X). rmv([X|Xs], Y, [X|Xs1]) :- rmv(Xs, Y, Xs1), pre_or_eq(X,Y). %Alternatively: find maximum, and then remove it. Both are acceptable solutions since no particular efficiency constraints are imposed in this subtask. %But we can easily write a version which combines the two cases: largest_and_remove(X, Y, [X|Xs], _, X, Xs) :- pre_or_eq(Y, X). largest_and_remove(X, Y, _, Ys, Y, [X|Ys]) :- pre(X, Y). rmv1(Xs, WithoutLargest) :- rmv1(Xs, _, WithoutLargest). rmv1([X], X, []). rmv1([X|Xs], Largest, WithoutLargest) :- rmv1(Xs, Y, WithoutY), largest_and_remove(X,Y, [X|Xs], WithoutY, Largest, WithoutLargest). %This looks complicated but the largest_and_remove/5 predicate can be obtained via recursive problem solving. Program for 3c: %Easy solution: find the maximum using the earlier predicate. Then define a predicate: rbm([], _, []). rbm([_|Xs], M, [M|Ms]) :- rbm(Xs, M, Ms). %This would not yield a full credit according to the problem description. A better solution is to simultaneously construct a list [M,M,...,M]. rbm1([X], X, M, [M]). rbm1([X|Xs], Largest, M, [M|Ms]) :- rbm1(Xs, Y, M, Ms), largest(X,Y,Largest). rbm1(Xs, Ms) :- rbm1(Xs, M, M, Ms). ######## Exercise 4 p(f(h(X, X))). p(h(V, f(V))). p(f(g(X))) :- p(h(X, Y)), p(Y). For exercises like this it is useful to test your answers with (e.g.) a query: call_with_depth_limit(p(X), 10, Res), write(p(X)), nl, fail. Note that this only works in SWI-Prolog. 4a: f(a), g(a), f(g(a)), ..., h(a,a), h(f(a), a),... UA is the set of all ground terms constructed out of symbols a, f, g, h. 4b: Yes. Clause 1 and 3 are ok since we have p(f(t)) for every ground term t. Clause 2 is ok. since we have p(h(t, f(t'))) for all t, t', and in particular for the case when t = t'. 4c: I1 = {p(f(h(t,t))), p(h(t,f(t))) | t \in UA}. I2 = I1 \cup {p(f(g(h(t,t)))) | t \in UA} (Motivation: body p(h(t, f(t))), p(f(t)) true in I1 yiels ground instance p(f(g(h(t,t)))) :- p(h(h(t,t), f(h(t,t)))), p(f(h(t,t)))). I3 = I2 \cup {p(f(g(g(h(t,t))))) | t \in UA} (Motivation: satisfying the first atom in the body yields p(h(h(t,t), f(h(t,t)))). The second atom is then p(f(t)) for some ground term t. Choosing t = g(h(t',t') for some ground term t' then works (implies that Y/g(h(t',t'))). The arbitrary case is then I_k = I_{k-1} \cup {p(f^(k-2 applications of g)(h(t,t)) | t \in UA}. 4d: p(f(g(g(a)))) 4e: p(h(a, a)) 4f: p(f(g(h(X,X)))) since p(f(g(h(t,t)))) is true for every ground term t. ######## Exercise 5: 5: We could e.g. choose the program: p(f(g(X))) :- p(h(X, Y)), p(Y). %Query: p(f(g(a))). %First computation rule: Prolog. Tree is finitely failed. %Second computation rule: rightmost atom. Goal p(Y) is always chosen => infinite tree. %More general advice: recall that your initial query may contain several goals. ######## Exercise 6: 6a: correctness means that whatever we have a (ground) consequence of the program then it must be included in the specification. The program is not correct with respect to the given specification and a simple counter example is p([], a). 6b Base case: let p([],s) be an arbitrary ground instance. Since [] does not contain any elements p([],s) is trivially included in the specification. Recursive case: let p([s|l1],[s|l2]) :- p(l1,l2) be an arbitrary ground instance. Assume that l1 = [s1, ..., sm] for some m >= 0, and that each si occurs as a subterm in l2. It follows that [s|l1] is a list and that each element is included in the term [s|l2]. Hence, p([s|l1],[s|l2]) is included in the specification under the stated assumptions. ######## Exercise 7: We are given the DCG y(0) --> []. y(s(X)) --> [0], y(X). y(s(X)) --> [1], y(X). and are asked to describe the language of y(s(s(s(0)))). It is not hard to see that intention of y(N) is to describe Boolean strings of length N (where N is represented by a unary term). Hence, y(s(s(s(0)))) contains all ternary Boolean strings, (e.g), 001. As usual, it is easiest to derive this string directly from the grammar, instead of translating to Prolog. y(s(s(X))) then contains all Boolean strings of length at least 2. ######## Exercise 8: o(s(0)). o(s(s(X))) :- ~e(X). e(0). e(X) :- ~o(X). In the following crude ASCII drawing * denotes the successful refutation. Query e(s(s(0))): e(s(s(0))) | ~o(s(s(0))) | * o(s(s(0))) -- FF (can be marked as FF since e(0) succeeded with the empty answer substitution). | ~e(0) e(0) -- Tree with two successful derivations. | | * ~o(0) | * o(0) -- FF Query e(s(s(X))): e(s(s(X))) | ~o(s(s(X))) | FLOUNDERED -- This leaf is floundered since o(X) is not finitely failed and does not contain a successful derivation with empty answer substitution. We realize this in the construction of o(s(s(X))) below. o(s(s(X))) | ~e(X) -- This leaf is floundered since the construction of e(X) failed. | FLOUNDERED e(X) /\ * ~o(X) -- In left branch we have substitution {X/0}. The right branch is floundered since | the construction of o(X) failed. FLOUNDERED o(X) /\ -- In left branch we have the substitution {X/s(0)} and in the right branch * ~e(X0) the substitution {X/s(s(X0))} for a fresh variable X0. | FLOUNDERED -- This leaf is floundered since the construction of e(X0) failed. e(X0) | FLOUNDERED -- This leaf is floundered since we are already attempting to construct e(X). Prolog would answer "yes" for e(s(s(X))). Why? Hint: Prolog does not check whether the empty answer substitution is obtained or not. What consequences does this have for the above trees? ######## Exercise 9: p :- ~q. q :- ~p. Herbrand interpretation Model? Stable model? {} No No {p} Yes Yes {q} Yes Yes {p,q} Yes No (To actually get credits on this task you also, in each interpretation, need to prove your claim. E.g., to prove that {p} is a stable model you need to compute the reduct of the program with respect to {p} and show that it is the least Herbrand model). SLDNF-trees: p q | | ~q ~p | | FLOUNDERED FLOUNDERED (Cannot conclude anything by SLDNF-resolution)