(i) (∀X)likes(chris,X)
(ii) (∃X)likes(X,chris) if (∀X)likes(X,X)
(iii) ¬(∃X)likes(X,X)
(i) (∀X)(even(X) or odd(X))
(ii) ¬(∃X)(even(X) & odd(X))
(iii) ¬(∃X)(0=s(X))
(iv) (∀X)(even(X) if odd(s(X)))
(v) (∀X)(even(X) iff ¬even(X))
(i) definite(X) or indefinite(X) or negative(X) or ¬clause(X)
(ii) ¬happy(chris) or ¬unhappy(chris)
(iii) happy(chris) or ¬happy(chris) or indifferent(chris)
(iv) ¬perfect(X)
(v) likes(X,Y) or ¬friends(X,Y)
(i) vertebrate(X) or invertebrate(X)
(ii) omniscient(god)
(iii) ¬True
(i) I've_seen(X) if I've_seen(Y) & elephant(Y) & flies(Y)
(ii) will_be_saved(X) or ¬repents(X) if True
(i) If X is a parent and X is a female then X is someone's mother.
(ii) If X is a father or X is a mother then someone is someone's parent.
(iii) If everyone is a parent then somebody is a child.
(i) two constants 'a' and 'b' and two 1-ary function symbols 'f' and 'g';
(ii) one constant 'a' and one 2-ary function symbol 't';
(iii) no constants but one 1-ary function symbol 'f'.
last(f(U,nil),U) last(f(U,Z),V) if last(Z,V)assuming that the language has just two constants 'nil' and 'a', and just one 2-ary function symbol 'f'.
last(f(a,f(a,nil)),a)
Note—an inference system is affirmation-complete if it can derive Q from P whenever Q is implied by P.
(i) apply {X/mum(Y), Y/chris} to likes(X,dad(Y))
(ii) apply {X/mum(chris), Y/chris} to likes(X,dad(Y))
(iii) apply {X/t(U,U), Y/U} to tree(t(X,t(Y,Y)))
(iv) apply {X/elizabeth} to (∃X)wife(X,Y) if man(Y) & married(Y,X)
(i) {X/mum(Y), Y/chris}
(ii) {X/X}
(iii) ø
(iv) {X/2, X/3}
(v) {X/2, X/2}
(vi) {X/Y, Y/X}
(vii) {X/2, Y/2, Y/X}
(viii) {f(X)/f(Y)}
σ = {X/f(a,Y), Y/f(b,Z), Z/c}determine the least value of n>0 for which σ^{n} is idempotent.
σ1 = {X/f(a,Y), W/f(U,Z)}
σ2= {X/f(a,a), Y/b, V/c}and confirm that Wσ* = (Wσ1)σ2 when W = p(V,X,Y,W).
path(X,Y) iff (go(Y) if go(X))
go(c) if go(b)
go(b) if go(a)Use resolution to refute ¬path(a,c).
C1: append(nil,W,W) C2: append(U•X,Y,U•Z) if append(X,Y,Z) Q: ? append(a•X•nil,Y•nil,Z)(i) rewrite Q in standard clause notation, showing all the relevant quantifiers;
(i) ? append(a•X•nil,Y•nil,Z)
(ii) ? append(a•X,Y,Z)
(iii) ? append(a•X,Y,b•Z)
(iv) ? append(X,a•Y,b•Z)
(v) ? append(X,nil,X•nil)
(vi) ? append(X,a•b•nil,Z) & append(a•b•nil,X,Z)
(vii) ? append(a•X,Y,Z) & append(Z,V,b•W)
Note—there is a trap in part (v).
one-and-zero(X) if ones(X) & zeros(X) ones(nil) ones(1•U•Y) if ones(Y) zeros(nil) zeros(U•0•Y) if zeros(Y)(i) Show the SLD-tree for the query ?one-and-zero(1•0•1•0•nil) under the computation rule which selects the lefmost literal. Would the computation rule which selects the rightmost literal be more efficient for the same query?
(ii) Which of those two computation rules is least efficient for executing the query ?one-and-zero(1•2•1•0•nil), and why?
(iii) If the interpreter can easily access and compare the lengths of arguments in calls, what new computation rule can you suggest which deals satisfactorily with both the above queries?
(i) p(a,X) and p(Y,b)
(ii) p(X,X) and p(Y,Z)
(iii) p(X,Y) and p(Y,X)
(iv) p(t(X,t(X,b))) and p(t(a,Z))
(v) p(t(X,t(X,b))) and p(t(a,t(Z,Z)))
(vi) p(X,f(Y)) and p(f(Y),X)
(vii) p(X,f(X)) and p(f(Z),f(Z))
An element can be appended to the end of a list in a single step provided that the given list is represented by a difference-list. In particular, the following query
? put_on_end(c,diff(a•b•X,X),L)can be solved to give the output binding L/a•b•c•nil by invoking a single assertion of the form
A: put_on_end(U,?,L)What do you suggest the assertion's second argument should be in order to produce this outcome? Investigate whether your suggested assertion also correctly solves the queries
Q1: ? put_on_end(c,diff(X,X),Y) and Q2: ? put_on_end(X,diff(X,X),Y)when the occur-check is in force. What happens when it is not?
S1: sort(Y,Y) if ord(Y) S2: sort(X,Y) if append3(X1,U•V•nil,X2,X) & V<U & append3(X1,V•U•nil,X2,Z) & sort(Z,Y)It works by repeatedly seeking disordered pairs of adjacent elements of the current list and correcting them. Here, ord(Y) means that Y is a list of numbers arranged in strictly ascending order, whilst append3(L1,L2,L3,L) means that L is the result of appending L3 to the result of appending L2 to L1. Assume that 'ord', 'append3' and '<' are defined correctly by further clauses supplementing S1 and S2. The intended meaning of sort(X,Y) is that Y is some permutation of X for which ord(Y) holds.
Comment upon the efficiency of this program for executing the standard query ?sort(3•1•4•2•nil,Y) under the standard strategy.
For the same query comment upon the correctness and efficiency of each of the three following adaptations of the above program:
(i) a cut inserted before the call V<U;
(ii) the cut inserted instead immediately after the call V<U;
(iii) as in (ii) but with S1 deleted and a new clause
S3: sort(Y,Y)placed after the clause S2.
Are there any standard queries which adaption (iii) would solve incorrectly relative to the intended meaning?
Note—in Questions 2–4 assume that P is definite.
A if ¬B & C
D if ¬C
¬D
list(nil)
list(a•X) if list(X)
p(X) if ¬p(Y)and say which, if any, are H-models for the clause.
append(nil,Z,Z)
append(U•X,Y,U•Z) if append(X,Y,Z)
append(X,nil,X)provided that X is a list.
num(0)use partial evaluation to derive the clause
num(s(U)) if num(U)
twice(0,0)
twice(s(U),s(s(Z))) if twice(U,Z)
even(Y) if num(X) & twice(X,Y)
even(s(s(Z))) if num(U) & twice(U,Z)
even(0)use unfolding to show that this is computationally equivalent to the program
odd(s(0))
even(s(X)) if odd(X)
odd(s(X)) if even(X)
even(0)
even(s(s(0)))
even(s(s(X))) if even(X)
odd(s(0))
odd(s(s(X))) if odd(X)
(ii) By partially evaluating the query ?even(X) show that the second clause of this new program is redundant.
one-and-zero(X) if ones(X) & zeros(X)
ones(nil)
ones(1•V•Y) if ones(Y)
zeros(nil)
zeros(U•0•Y) if zeros(Y)
(ii) Hence construct an argument to show that, for querying the predicate 'one-and-zero', this program is computationally equivalent to the program
one-and-zero(nil)
one-and-zero(1•0•Y) if one-and-zero(Y)
Note—assume in each case that H={dov,chris}.
(i) likes(chris,X) if likes(dov,X)
(ii) likes(chris,X) if ¬likes(X,chris)
(iii) likes(dov,X) or likes(X,chris)
(iv)
likes(dov,X)(v)
likes(X,chris)
¬likes(dov,dov)
likes(X,dov) if likes(chris,X)
likes(chris,X)
CWA(P) = P ∪ {¬likes(chris,dov),¬likes(chris,chris)}identify the simplest possible P which consists of
(i) two clauses;
(ii) one clause.