1. naloga ========= a) X = eva; X = tim; X = tina. b) bought(X, L), member(A/_, L), member(B/_, L), A \= B. c) total(Product, Amount, Value) :- findall(A, (bought(_, List), member(Product/A, List)), Amounts), sum(Amounts, Amount), price(Product, Price), Value is Amount * Price. 2. naloga ========= a) all_equal([]). all_equal([_]). all_equal([H,H|T]) :- all_equal([H|T]). b) p(L, SL) :- sublist(L, SL), all_equal(SL), length(SL, N1), \+ (sublist(L, SL2), all_equal(SL2), length(SL2, N2), N2 > N1). 3. naloga ========= a) all(A, animal(A) and not snake(A) ==> likes(mary, A)). b) exists(F, friend(F, peter) and all(R, restaurant(R) and good(R) and in(R, piran) ==> know(peter, R) and know(F, R))). c) exists(L, lady(L) and from(L, information_office) and all(T, tourist(T) and help(L, T) ==> exists(D, dog(D) and travel_with(T, D)))). 4. naloga ========= a) L = short; L = long. b) false. c) move(D) --> step(D). move(D) --> step(D1), move(D2), { D is D1 + D2 }. step(1) --> [short, up]. step(2) --> [long, up]. step(-1) --> [short, down]. step(-2) --> [long, down]. d) move(D) --> step(D). move(D) --> step(D1), move(D2), { D is D1 + D2 }. step(1) --> [short, up]. step(2) --> [long, up]. step(-1) --> [short, down]. step(-2) --> [long, down]. step(D) --> [repeat], move(D1), [X, times], { member(X/Y, [zero/0, one/1, two/2, three/3, four/4, five/5]), D is D1 * Y }. 5. naloga ========= a) Program P je parcialno pravilen glede na Φ in Ψ, če za vsak x velja: če Φ(x) in P se konča za x, potem velja Ψ(x, P(x)). Program P se izteče glede na Φ, če za vsak x velja: če Φ(x), potem se izvajanje programa konča. Program P je totalno pravilen glede na Φ in Ψ, če se (a) P izteče glede na Φ in (b) P je parcialno pravilen glede na Φ in Ψ. b) Cond je najšibkejši predpogoj, ki mora veljati pred stavkom Statement, da bo po izvršitvi Statement veljal PostCond. c) wp(INV, invariant INV while B do S, PostCond) :- % annotated while wp(Cond, S, INV), theorem(B and INV => Cond), % within loop theorem(not B and INV => PostCond). % exit from loop