Appendices

Appendix A describes a number of built-in Prolog predicates, and lists a library of utility programs. These predicates are used in various programs throughout the book.

Appendix B gives two programs converting to and from clausal logic. The first program transforms a formula in first-order Predicate Logic to clausal form, as described in section 2.5. The second program completes a given set of general clauses by means of Predicate Completion (section 8.2). The output of this program is a formula in Predicate Logic, which can be transformed back to clausal form by means of the first program.

Appendix C gives detailed answers to selected exercises.


A

A catalogue of useful predicates

Appendix A.1 describes a number of built-in Prolog predicates. Appendix A.2 comprises a small library of utility predicates that are used by programs in this book.

A.1  Built-in predicates

Term manipulation

Term1 = Term2          Term1 and Term2 are unified.

Term1 \= Term2        Term1 and Term2 cannot be unified.

Term1 == Term2        Term1 and Term2 are bound to the same term.

Term1 \== Term2      Term1 and Term2 are bound to different terms.

var(V)                        V is an unbound variable.

arg(N,T,A)                A is the N -th argument of term T.

functor(T,F,N)        T is a term with functor F and arity N.

Term =.. List          List is a list starting with the functor of Term, followed by its arguments.

varsin(Term,Vs)      Vs is a list of the variables in Term.

numbervars(T,N,M)  the variables in term T are instantiated to terms of the form '$VAR'( n ), where n is an integer which has a different value for each distinct variable. The variables will be numbered starting from N, and M is the next unused number.

Database manipulation

assert(Clause)        Clause is added at the end of the database (can also be a single atom, without a body).

asserta(Clause)      Clause is added at the top of the database.

clause(H,B)              H:-B is a clause in the database (H must be instantiated).

retract(Clause)      the first clause unifying with Clause is removed from the database.

retractall(Head)    all clauses with head unifying with Head are removed from the database.

kill(Predicate)      all clauses defining Predicate are removed from the database.

save(File)                save the clauses in the database to File.

consult(File)          load the clauses in File into the database.

op(P,Type,Name)    declare an operator Name with priority P (a number between 0 and 1200, lower priority binds stronger); Type is fx or fy for prefix, xfx, xfy or yfx for infix, and xf or yf for postfix.

Control

call(Goal)                call Goal (must be instantiated to a goal).

not(Goal)                  Goal is not provable (must be instantiated to a goal).
not/1 could be defined as
    not(Goal):-call(Goal),!,fail.
    not(Goal).

fail, false                forces failure.

true, otherwise        always succeeds.
true/0 could be defined as
    true.

repeat                        succeeds indefinitely many times on backtracking.
repeat/0 could be defined as
        repeat.
    repeat:-repeat.

findall(X,G,L)        L is a list of X ’s, one for each solution of G (succeeds with the empty list if no solutions are found).

bagof(X,G,L)            L is a list of X ’s, one for each solution of G, which may be preceded by existential variables (fails if no solutions are found).

setof(X,G,L)            as bagof/3, but L is a sorted list without duplicates.

forall(G,C)              for all the solutions of G, C is true.
forall/2 could be defined as
        forall(G,C):-not((G,not(C))).

Interaction

read(Term)                Term is instantiated to the next line typed by the user (must be a Prolog term).

write(Term)              write Term to the screen.

tab(N)                        write N spaces to the screen.

nl                                write a newline to the screen.

get(C)                        C is ASCII code of next character typed by the user.

put(C)                        write character with ASCII code C to the screen.

tell(File)                redirect output to File.

told                            stop redirecting output.

see(File)                  redirect input from File.

seen.                           stop redirecting input.


A.2  A library of utility predicates

What follows is a small collection of predicates that are used by various programs throughout the book.

Lists and sets.  We start with a couple of simple list predicates.

% element(X,Ys) <- X is an element of the list Ys

element(X,[X|Ys]).

element(X,[Y|Ys]):-
element(X,Ys).

% append(Xs,Ys,Zs) <- list Zs is Xs followed by Ys

append([],Ys,Ys).

append([X|Xs],Ys,[X|Zs]):-
append(Xs,Ys,Zs).

% remove_one(X,Ys,Zs) <- Zs is list Ys minus
%                       one occurrence of X

remove_one(X,[X|Ys],Ys).

remove_one(X,[Y|Ys],[Y|Zs]):-
remove_one(X,Ys,Zs).

The difference between lists and sets is that the order of elements in a set is not important. Thus, a subset is different from a sublist. The predicate proper_subset/2 works only if the first argument is a list without duplicates!

% subset(Xs,Ys) <- every element of Xs occurs in Ys

subset([],Ys).

subset([X|Xs],Ys):-
element(X,Ys),
subset(Xs,Ys).

% proper_subset(Xs,Ys) <- Xs is a subset of Ys, and Ys
%                        has more elements than Xs

proper_subset([],Ys):-
Ys \= [].

proper_subset([X|Xs],Ys):-
remove_one(X,Ys,Ys1),
proper_subset(Xs,Ys1).

The following three predicates use syntactic identity rather than unification, which is useful for lists containing variables.

var_element(X,[Y|Ys]):-
X == Y.   % syntactic identity

var_element(X,[Y|Ys]):-
var_element(X,Ys).

var_remove_one(X,[Y|Ys],Ys):-
X == Y.   % syntactic identity

var_remove_one(X,[Y|Ys],[Y|Zs]):-
var_remove_one(X,Ys,Zs).

var_proper_subset([],Ys):-
Ys \= [].

var_proper_subset([X|Xs],Ys):-
var_remove_one(X,Ys,Zs),
var_proper_subset(Xs,Zs).

Conjunctions and disjunctions.   Conjunctions and disjunctions are recursive datastructures, just like lists. However, whereas a single-element list such [1] is a complex term .(1,[]), a single-element conjunction or disjunction is a simple term. Therefore, each of the following predicates needs an extra clause for the single-element case. Note that true is the empty conjunction, while false represents the empty disjunction.

disj_element(X,X):-          % single-element disjunction
not X=false,
not X=(One;TheOther).

disj_element(X,(X;Ys)).

disj_element(X,(Y;Ys)):-
disj_element(X,Ys).

conj_append(true,Ys,Ys).

conj_append(X,Ys,(X,Ys)):-   % single-element conjunction
not X=true,
not X=(One,TheOther).

conj_append((X,Xs),Ys,(X,Zs)):-
conj_append(Xs,Ys,Zs).

disj_append(false,Ys,Ys).

disj_append(X,Ys,(X;Ys)):-   % single-element disjunction
not X=false,
not X=(One;TheOther).

disj_append((X;Xs),Ys,(X;Zs)):-
disj_append(Xs,Ys,Zs).

conj_remove_one(X,X,true):-  % single-element conjunction
not X=true,
not X=(One,TheOther).

conj_remove_one(X,(X,Ys),Ys).

conj_remove_one(X,(Y,Ys),(Y,Zs)):-
conj_remove_one(X,Ys,Zs).

Preventing variables from getting instantiated.   Whenever Prolog reads a clause from its internal database, fresh copies of the variables in the clause are created. When a meta-interpreter uses an internal list of clauses, this is desirable as well. The predicate copy_term/2 uses the internal database to create a fresh copy of any term. copy_element/2 uses copy_term/2 to create a fresh copy of an item in a list.

% copy_term(Old,New) <- New is a copy of Old
%                      with new variables

copy_term(Old,New):-
asserta('$copy'(Old)),
retract('$copy'(New)),!.

copy_term(Old,New):-   % in case Old and New don’t unify
retract('$copy'(Old)),
!,fail.

% copy_element(X,L) <- X is an element of L
%                     with new variables

copy_element(X,Ys):-
element(X1,Ys),
copy_term(X1,X).

try/1 is a meta-predicate which tests whether a goal succeeds, without returning an answer-substitution. This is achieved by taking advantage of the difference between negation as failure and logical negation.

% try(Goal) <- Goal succeeds, but variables
%             don’t get instantiated

try(Goal):-
not not Goal.

Various.   The remaining predicates speak for themselves.

% variant of setof/3 which succeeds with the empty list
% if no solutions can be found

setof0(X,G,L):-
setof(X,G,L),!.

setof0(X,G,[]).

% same_predicate(L1,L2) <- literals L1 and L2 have
%                         the same predicate and arity

same_predicate(L1,L2):-
functor(L1,P,N),
functor(L2,P,N).


B

Two programs for logical conversion

The program in appendix B.1 transforms a formula in first-order Predicate Logic to clausal form, as described in section 2.5. The program in appendix B.2 completes a given set of general clauses by means of Predicate Completion (section 8.2). The output of this program is a formula in Predicate Logic, which can be transformed back to clausal form by means of the first program.

B.1   From Predicate Logic to clausal logic

In section 2.5 we discussed a method for transforming a formula in Predicate Logic to an ‘almost’ equivalent set of clauses (reread this section if you don’t recall in what sense the clauses differ from the Predicate Logic formula). Below, a Prolog program implementing this method is given.

The logical symbols used in Predicate Logic formulas are defined as operators:

% logical symbols used in Predicate Logic formulas

:-op(900,xfx,'=>').         % implication

:-op(800,xfy,&).            % conjunction

:-op(800,xfy,v).            % disjunction

:-op(400,fy,-).             % negation

In addition, a universally quantified formula of the form X:F is represented by the term forall(X,F). For instance, the formula

S: student_of(S,peter) likes(peter,S)

is represented by

forall(S,student_of(peter)=>likes(peter,S)).

Likewise, an existentially quantified formula of the form X:F is represented by the term exists(X,F).

The tranformation from Predicate Logic to clausal logic requires six steps:

(i)   replace implications by disjunction and negation;

(ii)  push negations inside, so that each of them immediately precedes a literal;

(iii) move quantifiers to the front (the result is said to be in prenex normal form);

(iv) replace existentially quantified variables by Skolem functors;

(v)  rewrite into conjunctive normal form, i.e. a conjunction of disjunctions of literals;

(vi) rewrite each conjunct to a clause.

The main predicate transform/2 carries out these six steps:

transform(Formula,Clauses):-
rewrite_implications(Formula,F1),
negations_inside(F1,F2),
prenex_normal_form(F2,F3),
skolemise(F3,F4),
conjunctive_normal_form(F4,F5),
clausal_form(F5,Clauses).

Predicates for each of these steps are defined below.

The first two predicates contain one clause for each possible form a formula could have.

% rewrite_implications(F1,F2) <- F2 is a PL formula
%                               without implications,
%                               log. equivalent with F1

rewrite_implications(A,A):-           % base case
literal(A).

rewrite_implications(A => B, -C v D):-% implication
rewrite_implications(A,C),
rewrite_implications(B,D).

rewrite_implications(A & B, C & D):-  % no change;
rewrite_implications(A,C),       % try rest of
rewrite_implications(B,D).       % formula

rewrite_implications(A v B, C v D):-
rewrite_implications(A,C),
rewrite_implications(B,D).

rewrite_implications(-A,-C):-
rewrite_implications(A,C).

rewrite_implications(forall(X,B), forall(X,D)):-
rewrite_implications(B,D).

rewrite_implications(exists(X,B), exists(X,D)):-
rewrite_implications(B,D).

% negations_inside(F1,F2) <- F2 is a PL formula with
%                           negs. only preceding literals
%                           log. equivalent with F1

negations_inside(A,A):-               % base case
literal(A).

negations_inside(-(A & B), C v D):-   % De Morgan (1)
negations_inside(-A,C),
negations_inside(-B,D).

negations_inside(-(A v B), C & D):-  % De Morgan (2)
negations_inside(-A,C),
negations_inside(-B,D).

negations_inside(-(-A),B):-           % double negation
negations_inside(A,B).

negations_inside(-exists(X,A),forall(X,B)):- % quantifiers
negations_inside(-A,B).

negations_inside(-forall(X,A),exists(X,B)):-
negations_inside(-A,B).

negations_inside(A & B, C & D):-      % no change;
negations_inside(A,C),           % try rest of
negations_inside(B,D).           % formula

negations_inside(A v B, C v D):-
negations_inside(A,C),
negations_inside(B,D).

negations_inside(exists(X,A),exists(X,B)):-
negations_inside(A,B).

negations_inside(forall(X,A),forall(X,B)):-
negations_inside(A,B).

In step (iii), the quantifiers found at different positions in the formula are moved to the front, preserving their order. This is achieved by means of an auxiliary predicate pnf/4, which separates the quantifiers from the rest of the formula (referred to below as the Body). An additional argument V acts as a pointer to the place of the body in the quantifier structure. For instance, the query

?-pnf(forall(X,p(X,X)) & forall(Y,exists(Z,p(Y,Z))),Q,V,B)

has the following answers:

Q = forall(X,forall(Y,exists(Z,V)))
B = p(X,X)&p(Y,Z)

Unifying V with B gives the required formula in prenex normal form:

% prenex_normal_form(F1,F2) <- F2 is a PL formula
%                             with all quant.s in front,
%                             log. equivalent with F1

prenex_normal_form(F,PNF):-
pnf(F,PNF,B,B).

pnf(A,V,V,A):-               % base case
literal(A).

pnf(forall(X,F),forall(X,Quants),V,Body):-
pnf(F,Quants,V,Body).

pnf(exists(X,F),exists(X,Quants),V,Body):-
pnf(F,Quants,V,Body).

pnf(A & B,Quants,V,BodyA & BodyB):-
pnf(A,Quants,QB,BodyA),
pnf(B,QB,V,BodyB).

pnf(A v B,Quants,V,BodyA v BodyB):-
pnf(A,Quants,QB,BodyA),
pnf(B,QB,V,BodyB).

Step (iv) is called Skolemisation. It involves introducing a Skolem functor for each existentially quantified variable. The Skolem functors are named sk1, sk2, etc. The arguments of the Skolem functors are given by the universally quantified variables found before the existentially quantified one. Since all remaining variables are universally quantified, the universal quantifiers can be dropped. (Strictly speaking, the formula is now neither in Predicate Logic form, nor in clausal form.)

% skolemise(F1,F2) <- F2 is obtained from F1 by replacing
%                    all existentially quantified
%                    variables by Skolem terms

skolemise(F1,F2):-
skolemise(F1,[],1,F2).

skolemise(forall(X,F1),VarList,N,F2):-!,% remove univ.
skolemise(F1,[X|VarList],N,F2).     % quantifier

skolemise(exists(X,F1),VarList,N,F2):-!,
skolem_term(X,VarList,N),           % unify with
N1 is N+1,                          % Skolem term
skolemise(F1,VarList,N1,F2).

skolemise(F,V,N,F).          % copy rest of formula

skolem_term(X,VarList,N):-
C is N+48,                   % number -> character
name(Functor,[115,107,C]),   % Skolem functor skN
X =.. [Functor|VarList].

We now have a formula containing only conjunction, disjunction and positive and negative literals. Such a formula can uniquely be rewritten to a conjunction of disjunctions of literals, by distributing disjunction over conjunction. The result is said to be in conjunctive normal form (CNF):

conjunctive_normal_form(A,A):-              % base case
disjunction_of_literals(A),!.

conjunctive_normal_form((A & B) v C, D & E ):-!,
conjunctive_normal_form(A v C,D),      % distribution
conjunctive_normal_form(B v C,E).

conjunctive_normal_form(A v (B & C), D & E ):- !,
conjunctive_normal_form(A v B,D),      % distribution
conjunctive_normal_form(A v C,E).

conjunctive_normal_form(A & B,C & D):-      % conjuction
conjunctive_normal_form(A,C),
conjunctive_normal_form(B,D).

conjunctive_normal_form(A v B,E):-          % other cases
conjunctive_normal_form(A,C),
conjunctive_normal_form(B,D),
conjunctive_normal_form(C v D,E).

Finally, the CNF-formula is rewritten to a list of clauses. For simplicity, body and head of each clause are represented by lists:

clausal_form(A,[Clause]):-
disjunction_of_literals(A),
make_clause(A,Clause).

clausal_form(A & B,Clauses):-
clausal_form(A,ClausesA),
clausal_form(B,ClausesB),
append(ClausesA,ClausesB,Clauses).

make_clause(P,([P]:-[])):-
logical_atom(P).

make_clause(-N,([]:-[N])):-
logical_atom(N).

make_clause(A v B,(HeadAB:-BodyAB)):-
make_clause(A,(HeadA:-BodyA)),
make_clause(B,(HeadB:-BodyB)),
append(HeadA,HeadB,HeadAB),
append(BodyA,BodyB,BodyAB).

The program is completed by a number of simple utility predicates:

disjunction_of_literals(A):-
literal(A).

disjunction_of_literals(C v D):-
disjunction_of_literals(C),
disjunction_of_literals(D).

literal(A):-
logical_atom(A).

literal(-A):-
logical_atom(A).

logical_atom(A):-
functor(A,P,N),
not logical_symbol(P).

logical_symbol(=>).

logical_symbol(<=>).

logical_symbol(-).

logical_symbol(&).

logical_symbol(v).

logical_symbol(exists).

logical_symbol(forall).

B.2   Predicate Completion

In section 8.2, we presented Predicate Completion as a technique for explicitly handling negative information. A logic program is viewed as a set of predicate definitions, where the only-if parts are implicitly assumed. Below, a program is given which constructs additional clauses representing the only-if parts.

A program is represented as a list of clauses, where head and body of each clause are lists of atoms, as in the program in the previous section. The output of the Predicate Completion program is a formula in first-order Predicate Logic, which can be transformed to clausal logic by means of the aforementioned program, if desired. Definitions for different predicates are handled separately, so the first step is to partition the program into separate predicate definitions. After completing each of these definitions we add appropriate formulas for each of the undefined predicates.

% complete(P,F) <- P is a list of predicate definitions,
%                 and F is a Predicate Logic formula
%                 representing the only-if parts of P

complete(Program,Comp):-
separate_definitions(Program,Definitions),
complete_definitions(Definitions,CompDefs,Heads),
handle_undefined(Program,Heads,CompDefs,Comp).

separate_definitions([],[]).

separate_definitions([([H]:-B)|Cls],[[([H]:-B)|D]|Ds]):-
get_definition(Cls,H,D,Rest),
separate_definitions(Rest,Ds).

get_definition([],Head,[],[]).

get_definition([([H]:-B)|Cls],Head,[([H]:-B)|Def],Rest):-
same_predicate(H,Head),
get_definition(Cls,Head,Def,Rest).

get_definition([([H]:-B)|Cls],Head,Def,[([H]:-B)|Rest]):-
not same_predicate(H,Head),
get_definition(Cls,Head,Def,Rest).

Undefined predicates are those which occur in bodies of clauses without occurring in any head. The list Heads of defined predicates is obtained while completing each predicate definition. Care must be taken to avoid considering not/1 as an undefined predicate, and also to check the negated literal itself. After constructing the list of undefined literals occuring in clause bodies, each of them is transformed into a formula of the form X1 Xn: ¬ p(X1,…,Xn):

handle_undefined(Program,Heads,CompDefs,Comp):-
findall(L,
       ( member((H:-B),Program),% pick a clause body
         ( (member(L,B),not L=not(X)) % unneg. lit.
         ; member(not L,B) ),   % or a negated one
         not member(L,Heads) ), % which is undefined
      Undefs),
undef_formulas(Undefs,CompDefs,Comp).

undef_formulas([],Comp,Comp).

undef_formulas([L|Ls],Comp0,Comp):-
quantify(L,F),
undef_formulas(Ls,F & Comp0,Comp).

quantify(L,F):-
L =.. [P|As],
variablise(As,Vs,F,-NewL),   % NB. negation symbol!
NewL =.. [P|Vs].    % turn arguments into variables

% add quantifiers

variablise([],[],L,L).

variablise([A|As],[V|Vs],forall(V,F),L):-
variablise(As,Vs,F,L).

The main task in Predicate Completion is the completion of each separate predicate definition. The main steps are

(i)   adding explicit unifications to the body of clauses;

(ii)  adding existential quantifiers for those variables occurring in the body of a clause but not in its head;

(iii) combining the clauses into one formula, and adding universal quantifiers for the head variables.

The predicate unifications_and_quantifiers/2 takes care of the first two steps, and the third step is carried out by the predicate complete_formula/3. These predicates are relatively self-explanatory:

% complete_definitions(D,C,H) <- C is the complement of
%                               definitions D, and H is
%                               list of variablised heads

complete_definitions([Def],Comp,[Head]):-!,
complete_definition(Def,Comp,Head).

complete_definitions([Def|Defs],Comp & Comps,[H|Hs]):-
complete_definition(Def,Comp,H),
complete_definitions(Defs,Comps,Hs).

complete_definition(Definition,Comp,Head):-
unifications_and_quantifiers(Definition,F),
complete_formula(F,Comp,Head).

unifications_and_quantifiers([],[]).

unifications_and_quantifiers([Clause|Clauses],[C|Cs]):-
unifs_and_quants(Clause,C),
unifications_and_quantifiers(Clauses,Cs).

unifs_and_quants(([Head]:-Body),([NewHead]:-NewBody)):-
Head=..[Pred|Args],
explicit_unifications(Args,NewArgs,Body,TmpBody),
existential_quantifiers(TmpBody,NewArgs,NewBody),
NewHead=..[Pred|NewArgs].

% explicit_unifications(A,NA,B,NB) <- NA is list A with
%                          non-var. terms replaced by new
%                          var.s; NB is body B extended
%                          with explicit unifications

explicit_unifications([],[],Body,Body).

explicit_unifications([T|As],[V|NewAs],B,[V=T|NewB]):-
nonvar(T),               % add explicit unification
explicit_unifications(As,NewAs,B,NewB).

explicit_unifications([Var|As],[Var|NewAs],Body,NewBody):-
var(Var),                % no expl. unific. needed
explicit_unifications(Args,NewArgs,Body,NewBody).

% existential_quantifiers(B,V,NB) <- NB is conj. of lit.s
%                           in B, extended by ex. quant.s
%                           for var.s in B but not in V

existential_quantifiers(Body,HeadVars,NewBody):-
varsin(Body,BodyVars),       % built-in predicate
body_form(Body,Conj),        % list -> conjunction
body_quants(BodyVars,HeadVars,Conj,NewBody).

body_form([not Lit],-Lit):-!.

body_form([Lit],Lit):-!.

body_form([not Lit|List],-Lit & Conj):-!,
body_form(List,Conj).

body_form([Lit|List],Lit & Conj):-
body_form(List,Conj).

% body_quants(BV,HV,C,QC) <- QC is conj. C extended with
%                           existential quant.s for all
%                           variables in BV but not in HV

body_quants([],HeadVars,Conj,Conj).

body_quants([BVar|BVars],HeadVars,Conj,exists(BVar,F)):-
not var_element(BVar,HeadVars),
body_quants(BVars,HeadVars,Conj,F).

body_quants([BVar|BVars],HeadVars,Conj,F):-
var_element(BVar,HeadVars),
body_quants(BVars,HeadVars,Conj,F).

% complete_formula(C,F,H) <- F is disjunction of bodies
%                           of clauses in C, and univ.
%                           quantified head H

complete_formula(C,Formula,Head):-
combine_clauses(C,Head,Body),
varsin(Head,HeadVars),
head_quants(HeadVars,Head => Body,Formula).

combine_clauses([([Head]:-Body)],Head,Body):- !.

combine_clauses([([Head]:-Body)|R],Head,Body v RBody):-
combine_clauses(R,Head,RBody).

head_quants([],Formula,Formula).

head_quants([HVar|HVars],Formula,forall(HVar,F)):-
head_quants(HVars,Formula,F).

The following query illustrates the operation of the program, and shows also how it can be combined with the program for conversion to clausal form presented in the previous section.

?-P=[([bird(tweety)]:-[]),
  ([flies(X)]:-[bird(X),not abnormal(X)])],
complete(P,F),
transform(F,C).

F=forall(Y,-abnormal(Y)) &
forall(Z,bird(Z) => Z=tweety) &
forall(X,flies(X) => bird(X) & -abnormal(X))

C=[([]:-[abnormal(Y)]),
 ([Z=tweety]:-[bird(Z)]),
 ([bird(X)]:-[flies(X)]),
 ([]:-[flies(X),abnormal(X)])]


C

Answers to selected exercises

Below, answers to selected exercises can be found. Not all answers have been included, due to two reasons. Some of the questions only lead to a new insight when the answer is actually constructed, and the student is encouraged to do so. Furthermore, some other questions embody small programming projects, and don’t have straightforward answers.

The remaining questions have been constructed to highlight a particular point in the discussion (which, incidentally, is the reason that they are printed throughout the text, and not at the end of each chapter). They are most advantageous when addressed as soon as they are encountered. The answers provided here can then be used to check and assess one’s own solution. Most of the answers contain additional explanatory remarks.

Alternatively, this appendix can be read separately, after the previous chapters have been studied. To this end, some of the questions have been reformulated so as to minimise references to the original text.

C.1  A brief introduction to clausal logic

Exercise 1.2. Construct the proof trees for the query
                                          ?-nearby(W,charing_cross).

There are six answers to this query:

{ W green_park }
{ W piccadilly_circus }
{ W leicester_square }
{ W bond_street }
{ W oxford_circus }
{ W tottenham_court_road }

The proof trees for the first three answers are analogous to fig. 1.2. The proof tree for the fourth answer is given below (the two remaining proof trees are similar):

Exercise 1.4. A list is either the empty list [], or a non-empty list [First|Rest] where Rest is a list. Define a relation list(L), which checks whether L is a list. Adapt it such that it succeeds only for lists of (i) even length and (ii) odd length.

The first specification can immediately be translated to Prolog:

list([]).

list([First|Rest]):-list(Rest).

A list of even length is either the empty list, or a non-empty list with two more elements than the next shorter list of even length:

evenlist([]).

evenlist([First,Second|Rest]):-evenlist(Rest).

In order to adapt this definition for lists of odd length, only the non-recursive clause needs to be changed:

oddlist([One]).

oddlist([First,Second|Rest]):-oddlist(Rest).

Notice that oddlist can also be defined in terms of evenlist (or vice versa):

oddlist([First|Rest]):-evenlist(Rest).

Exercise 1.5. Construct a query asking for a route from Bond Street to Piccadilly Circus with at least two intermediate stations.

?-reachable(bond_street,piccadilly_circus,[S1,S2|Rest]).

C.2  Clausal logic and resolution: theoretical backgrounds

Exercise 2.1. Translate the following statements into clauses, using the atoms person, sad and happy:
(a)    persons are happy or sad;
(b)    no person is both happy and sad;
(c)    sad persons are not happy;
(d)    non-happy persons are sad.

The statements should be read as ‘ ifthen …’ statements. Thus, the first statement reads ‘ if somebody is a person, then she is happy or sad’:

(a)   happy;sad:-person

The second statement reads ‘ if somebody is a person, then she is not both happy and sad’. In clausal logic, only positive conclusions can be drawn; negative conclusions are turned into positive conditions, as follows: ‘ if somebody is a person, and she is happy and sad, then contradiction’. A contradictory conclusion is signalled by the empty head:

(b)  :-person,happy,sad

Following the same recipe, the third statement expresses that ‘ if somebody is a person who is sad, and she is happy, then contradiction’:

(c)   :-person,sad,happy

Thus, sentences (b) and (c) convey the same logical meaning.

Finally, the fourth sentence reads ‘ if somebody is a person who is not happy, then she is sad’. In clausal logic, only positive conditions can be used; therefore, this negative condition should be turned into a positive conclusion: ‘ if somebody is a person, then she is sad or happy’. We thus obtain the same clause as in case (a):

(d)   sad;happy:-person

Exercise 2.2. Given the program
                                          married;bachelor:-man,adult.
                man.
                :-bachelor.

determine which of the following clauses are logical consequences of this program:
(a)    married:-adult;
(b)    married:-bachelor;
(c)    bachelor:-man;
(d)    bachelor:-bachelor.

(a) Any model of the first clause, which additionally makes man true, is also a model of the clause married;bachelor:-adult. Likewise, any model of this clause which additionally makes bachelor false is also a model of the clause married:-adult, which is therefore a logical consequence of the program.

(b) The body of this clause is false in any model of the program, and therefore the clause is true in any such model.

(c) The body of this clause is true in any model of the program, while its head is false. The clause is therefore not a logical consequence of the program (on the contrary, it is false in every model of the program, not just in some).

(d) This clause is a tautology: it is true in any interpretation, and therefore a logical consequence of any program.

Exercise 2.3. Write down the six Herbrand interpretations that are not models of the program
                married;bachelor:-man,adult.
                has_wife:-man,married.

The six interpretations are:

{ man , adult }
{ man , adult , has_wife }
{ man , married }
{ man , married , adult }
{ man , married , bachelor }
{ man , married , adult , bachelor }

The first two interpretations satisfy the body of the first clause but violate its head; the remaining four interpretations satisfy the body of the second clause but violate its head.

Exercise 2.4. Give a derivation of friendly from the following program:
                                          happy;friendly:-teacher.
                friendly:-teacher,happy.
                teacher;wise.
                teacher:-wise.

This requires derivations of the clauses friendly:-teacher and teacher:

Notice that this derivation can not be recast in the form of a linear tree, where each resolvent is obtained from the previous resolvent and a given clause, as in Chapter 1. This is due to the fact that some clauses are indefinite (have more than one positive literal).

Exercise 2.5. Prove by refutation that friendly:-has_friends is a logical consequence of the following clauses:
                                          happy:-has_friends.
                friendly:-happy.

The negation of friendly:-has_friends consists of two clauses, :‑friendly and has_friends. Together, these four clauses are inconsistent:

Exercise 2.6. How many models does the following clause have over the Herbrand universe { peter, maria }:
                                          likes(peter,S):-student_of(S,peter)

The set of ground instances of this clause is

{ likes(peter,maria):-student_of(maria,peter) ,
likes(peter,peter):-student_of(peter,peter) }

and the Herbrand base is

likes(peter,peter) , likes(peter,maria) ,
likes(maria,peter) , likes(maria,maria) ,
student_of(peter,peter) , student_of(peter,maria) ,
student_of(maria,peter) , student_of(maria,maria) }

Only the left four ground atoms are relevant for determining whether an interpretation is a model. 9 out of 16 truth-value assignments to these ground atoms result in a model. Because of the 4 irrelevant ground atoms, this yields 9*2 4 =144 models. Notice that this is a rather large number of models for such a modest Herbrand universe, and such a simple clause! This illustrates that less knowledge leads to more models.

Exercise 2.7. Write a clause expressing that Peter teaches all the first-year courses, and apply resolution to this clause and the clause
                                          likes(peter,maria):-follows(maria,C),teaches(peter,C)

This is expressed by the clause

teaches(peter,C):-first_year_course(C)

Resolution with the above clause yields

likes(peter,maria):-follows(maria,C),first_year_course(C)

In words: ‘Peter likes Maria if Maria follows a first-year course’.

Exercise 2.9. Translate to clausal logic:
(a)    every mouse has a tail;
(b)    somebody loves everybody;
(c)    every two numbers have a maximum.

(a) This statement should be read as ‘ if X is a mouse, then there exists something which is X ’s tail’. Giving X ’s tail the abstract name tail(X), we obtain the following clause:

tail_of(tail(X),X):-mouse(X)

(b) Here we need to give the person who loves everybody an abstract name. Since this person does not depend on anybody else, it can simply be a constant:

loves(person_who_loves_everybody,X)

Notice the difference with the statement ‘everybody loves somebody’:

loves(X,person_loved_by(X))

(c) This statement should be read as ‘ if X and Y are numbers, then there exists a number which is their maximum’. Giving this maximum the abstract name max(X,Y) yields the clause

maximum(X,Y,max(X,Y)):-number(X),number(Y)

Exercise 2.10. Determine the Herbrand universe of the following program:
                                          length([],0).
                length([X|Y],s(L)):-length(Y,L).
(Hint: recall that [] is a constant, and that [X|Y] is an alternative notation for the complex term .(X,Y) with binary functor ‘ . ’!)

In the intended interpretation, s is restricted to numbers and ‘ . ’ is restricted to lists; however, variables are untyped in clausal logic, and the two sets of terms may be mixed. Thus, the Herbrand universe will contain terms denoting numbers, such as

0 , s(0) , s(s(0)) , s(s(s(0))) , …

and terms denoting lists of numbers, such as

[] , [0] , [s(0),0] , [s(s(0)),s(0),0] , …

but also ‘strange’ terms like

[[[0]]] or .(.(.(0,[]),[]),[])
[s(0)|0] or .(s(0),0)
[s([[]|0])]

and so on.

Exercise 2.11. If possible, unify the following pairs of terms:
(a)    plus(X,Y,s(Y)) and plus(s(V),W,s(s(V)));
(b)    length([X|Y],s(0)) and length([V],V);
(c)    larger(s(s(X)),X) and larger(V,s(V)).

(a) plus(s(V),s(V),s(s(V))).

(b) length([s(0)],s(0)).

(c) Not unifiable.

Exercise 2.13. Write a clause for the statement ‘somebody is innocent unless proven guilty’, and give its intended model (supposing that john is the only individual in the Herbrand universe).

The clause is

innocent(X):-not guilty(X)

with intended model { innocent(john) }.

Exercise 2.14. Translate to clausal logic:
(a)     X Y: mouse(X) tail_of(Y,X);
(b)     X Y: loves(X,Y) ( Z: loves(Y,Z));
(c)     X Y Z: number(X) number(Y) maximum(X,Y,Z).

(a) This statement translates almost immediately into a clause, replacing the existential quantifier by a Skolem functor tail:

tail_of(tail(X),X):-mouse(X)

(b) This formula is already in conjunctive normal form, and each conjunct yields a separate clause. After replacing the existential quantifier by a Skolem functor person_loved_by, we obtain

loves(X,person_loved_by(X)).
loves(person_loved_by(X),Z).

Notice that the two clauses are ‘linked’ by the Skolem functor.

(c) Here, the Skolem functor has two arguments:

maximum(X,Y,max(X,Y)):-number(X),number(Y)

See also Exercise 2.9.

C.3  Logic Programming and Prolog

Exercise 3.2. Draw the SLD-tree for the following program:
                                          list([]).
                list([H|T]):-list(T).

and the query ?-list(L).

This is one of the simplest infinite SLD-trees:

The query succeeds infinitely often, producing the answers:

L = [];
L = [X1,X2];
L = [Y1,Y2,Y3];
L = [Z1,Z2,Z3,Z4];

and so on. Note that reversing the order of the clauses means that Prolog gives no answer at all.

Exercise 3.3. Draw the SLD-tree for the query ?-likes(A,B), given the following program:
                likes(peter,Y):-friendly(Y).
                likes(T,S):-student_of(S,T).
                student_of(maria,peter).
                student_of(paul,peter).
                friendly(maria).
Add a cut in order to prune away one of the answers { A peter, B maria }, and indicate the result in the SLD-tree. Can this be done without pruning away the third answer?

This program produces three answers:

 

 

 

Adding a cut to the first clause (before or after friendly(Y)) will prune away two answers (left figure). Adding a cut to the second clause can be done in two places: placing it just before the literal student_of(S,T) has no effect, while placing it at the end will only prune the answer { A peter, B paul } (right figure).

 

 

If in addition the two student_of clauses are swapped, only the second answer { A peter, B maria } is pruned.

Exercise 3.5. Given the program
                bachelor(X):-not(married(X)),man(X).
                man(fred).
                man(peter).
                married(fred).
draw the SLD-trees for the queries ?-bachelor(fred) and ?‑bachelor(peter).

Exercise 3.6. Change the first clause to
                bachelor(X):-not(married(X)),man(X)
and show that the modified program produces the right answer, by drawing the SLD-tree for the query ?-bachelor(X).

Exercise 3.7. Given the program
                                          p:-q,r,s,!,t.
                p:-q,r,u.
                q.
                r.
                u.
show that the query ?-p succeeds, but that q and r are tried twice.

Exercise 3.8. Given the equivalent program with if-then-else
                                          p:-q,r,if_s_then_t_else_u.
                if_s_then_t_else_u:-s,!,t.
                if_s_then_t_else_u:-u.
show
that q and r are now tried only once.

Exercise 3.9. Write a predicate zero(A,B,C,X) which, given the coefficients a, b and c, calculates both values of x for which ax 2 + bx + c =0.

zero(A,B,C,X):-
X is (-B + sqrt(B*B - 4*A*C)) / 2*A.

zero(A,B,C,X):-
X is (-B - sqrt(B*B - 4*A*C)) / 2*A.

Exercise 3.10. Given the program
                                          length([],0).
                length([H|T],N):-length(T,M),N is M+1.
draw the proof tree for the query ?-length([a,b,c],N).

Notice that the maximum number of literals in the resolvent is proportional to the depth of the recursion, which is typical for non-tail recursive predicates. When proofs are long, such programs will be quite inefficient.

Exercise 3.11. Given the program
                    length_acc(L,N):-length_acc(L,0,N).
       length_acc([],N,N).
       length_acc([H|T],N0,N):-N1 is N0+1,length_acc(T,N1,N).
draw the proof tree for the query ?-length_acc([a,b,c],N).

In this program, the is literals are solved immediately after they are added to the resolvent:

Here, the length of the resolvent is independent of the level of recursion, which makes tail-recursive loops very similar to iterative loops with regard to memory requirements.

Exercise 3.13. In the naive_reverse predicate, represent the reversed list by a difference list, use append_dl instead of append, and show that this results in the predicate reverse_dl by unfolding the definition of append_dl.

The reversed lists are represented by difference lists as follows:

•     (partly) specified lists are extended with a variable representing the minus list, e.g. [] becomes R-R, and [H] becomes [H|Minus]-Minus;

•     a variable representing a list is replaced by two variables representing the plus and minus lists, e.g. R becomes RPlus-RMinus.

reverse([],R-R).

reverse([H|T],RPlus-RMinus):-
reverse(T,R1Plus-R1Minus),
append_dl(R1Plus‑R1Minus,[H|Minus]‑Minus,RPlus‑RMinus).

Unfolding the call to append_dl/3 means that R1Plus should be unified with RPlus, R1Minus with [H|Minus], and Minus with RMinus, which yields

reverse([],R-R).

reverse([H|T],RPlus-RMinus):-
reverse(T,RPlus-[H|RMinus]).

Renaming the variables results in the same definition as reverse_dl/2.

This illustrates that the translation from simple lists to difference lists can (to a large extent) be automated.

Exercise 3.14. Rewrite the program for rel, using =..

rel(R,[],[]).

rel(R,[X|Xs],[Y|Ys]):-
Goal =.. [R,X,Y],
call(Goal),
rel(R,Xs,Ys).

Note that, in contrast with the original program, this program conforms to the syntax of clausal logic: there are no variables in functor or literal positions.

Exercise 3.15. Write a program which sorts and removes duplicates from a list, using setof.

The basic idea is to use element/2 to generate the elements of the list on backtracking, and to collect and sort them by means of setof/2.

sort(List,SortedList):-
setof(X,element(X,List),SortedList).

element(X,[X|Ys]).

element(X,[Y|Ys]):-
element(X,Ys).

Exercise 3.18. Implement a predicate permutation/2, such that permutation(L,P) is true if P contains the same elements as the list L but (possibly) in a different order, following these steps. (One auxiliary predicate is needed.)

As usual, we start with the declarative specification:

% permutation(L,P) <- P contains the same elements as L
%                    (possibly in a different order)

Taking the first argument as the recursion argument and the second as the output argument, we obtain the following skeleton:

permutation([],[]).

permutation([Head|Tail],?Permutation):-
/* do something with Head */
permutation(Tail,Permutation).

Inserting Head somewhere in Permutation should yield ?Permutation:

permutation([],[]).

permutation([Head|Tail],WholePermutation):-
insert_somewhere(Head,Permutation,WholePermutation),
permutation(Tail,Permutation).

The predicate insert_somewhere/3 can be obtained in the same way as the predicate insert/3 (section 3.9) by ignoring the arithmetic conditions:

insert_somewhere(X,[],[X]).

insert_somewhere(X,[Head|Tail],[Head|Inserted]):-
insert_somewhere(X,Tail,Inserted).

insert_somewhere(X,[Head|Tail],[X,Head|Tail]).

This program, which is declaratively and procedurally correct, can be slightly improved by noting that the first and third clauses can be combined into a single base case:

insert_somewhere(X,List,[X|List]).

insert_somewhere(X,[Head|Tail],[Head|Inserted]):-
insert_somewhere(X,Tail,Inserted).

Exercise 3.19. Implement an alternative sorting method by using the partition/4 predicate.

This predicate implements the famous quicksort algorithm, which is one of the most efficient sorting algorithms:

quicksort([],[]).

quicksort([X|Xs],Sorted):-
partition(Xs,X,Littles,Bigs),
quicksort(Littles,SortedLittles),
quicksort(Bigs,SortedBigs),
append(SortedLittles,[X|SortedBigs],Sorted).

The program can still be improved by employing difference lists.

C.4  Representing structured knowledge

The exercises in this chapter should not provide major difficulties.

C.5  Searching graphs

Exercise 5.3. Consider the following program:
                brother(peter,paul).
                brother(adrian,paul).
                brother(X,Y):-brother(Y,X).
                brother(X,Y):-brother(X,Z),brother(Z,Y).
Compare and explain the behaviour of prove_bf/1 and Prolog on the query ?‑brother(peter,adrian). Can you re-order the clauses, such that Prolog succeeds?

Prolog will be trapped in an infinite loop, regardless of the order of the clauses. This is so because a refutation of ?‑brother(peter,adrian) requires both recursive clauses, but whichever is found first will also be tried before the second one in all the other refutation steps. In contrast, prove_bf/1 will be able to construct a refutation.

Exercise 5.5. Give the models of the program
                married(X);bachelor(X):-man(X),adult(X).
                has_wife(X):-married(X),man(X).
                man(paul).
                adult(paul).

This program has four models (bachelors may have a wife, and married man may be bachelors):

{ man(paul) , adult(paul) , bachelor(paul) }
{
man(paul) , adult(paul) , bachelor(paul) , has_wife(paul) }
{
man(paul) , adult(paul) , married(paul) , has_wife(paul) }
{
man(paul) , adult(paul) , married(paul) , bachelor(paul) ,
 
has_wife(paul) }

The second and fourth models are non-minimal.

Exercise 5.6. Are all minimal models always constructed by model/1?

Yes. The set of all Herbrand interpretations can be seen as a search space, in which the models are to be found. This search space is ordered by the subset relation. model/1 starts from the empty interpretation, and repeatedly adds ground atoms until a model is constructed. Since one atom is added at a time, the procedure will never jump over a model. Since, on backtracking, all possible ways to satisfy a violated clause are considered, model/1 performs a breadth-first search (which is complete).

C.6  Informed search

Exercise 6.1. Suppose the call children(Current,Children) results in an ordered list of children. Write a predicate merge/3 which directly merges this list with the current agenda.

This predicate is a little bit special because it requires two recursion arguments. Therefore, there are two recursive clauses and two base cases. Note that in the second clause the first argument is required to be a non-empty list. This is done to prevent the query ?‑merge([],[],L) from succeeding twice.

merge([],Agenda,Agenda).

merge([Child|Children],[],[Child|Children]).% empty agenda

merge([Child|Children],[Node|Agenda],[Child|NewAgenda]):-
eval(Child,ChildValue),
eval(Node,NodeValue),
ChildValue < NodeValue, % Child is better than Node
merge(Children,[Node|Agenda],NewAgenda).

merge([Child|Children],[Node|Agenda],[Node|NewAgenda]):-
eval(Child,ChildValue),
eval(Node,NodeValue),
ChildValue >= NodeValue,% Child not better than Node
merge([Child|Children],Agenda,NewAgenda).

Exercise 6.4. Find a position for which the third heuristic is too pessimistic.

It is too pessimistic for the starting position (minimal cost 15, estimate 18).

C.7  Reasoning with natural language

Exercise 7.1. Redraw the parse tree of fig. 7.1 in the manner of an SLD proof tree, where ‘resolvents’ are partially parsed sentences such as
                                          [the],[rapid],noun,verb_phrase
and ‘clauses’ are grammar rules.

Exercise 7.2. Draw the search space generated by the grammar in section 7.1 for a top-down parse, if grammar rules are applied to sentences from left to right. Discuss the similarities and differences with SLD-trees.

The search space is partly drawn below; the lower part, which contains all possible verb phrases, re-appears at three other nodes as indicated.

This search space is basically a propositional SLD-tree, with fully parsed sentences corresponding to success branches (failure branches occur only when for some syntactic category no grammar rules are specified).

Exercise 7.4. Extend the following grammar rules with arguments expressing their interpretation:
       verb_phrase     --> transitive_verb,proper_noun.
       transitive_verb --> [likes].

The transitive verb defines a binary mapping Y=>X=>L, which is applied to the meaning of the proper noun:

verb_phrase(M) --> transitive_verb(Y=>M),proper_noun(Y).
transitive_verb(Y=>X=>likes(X,Y)) --> [likes].

C.8  Reasoning with incomplete information

Exercise 8.1. Give the models of the program
                bird(tweety).
                ostrich(tweety).
                flies(X):-bird(X),not abnormal(X).
                abnormal(X):-ostrich(X).
(interpreting the general clause as the corresponding indefinite clause). Which one is the intended model (see section 2.4)?

The models are

{ bird(tweety) , ostrich(tweety) , abnormal(tweety) }
{ bird(tweety) , ostrich(tweety) , abnormal(tweety) ,
 
flies(tweety) }

i.e. Tweety, being an ostrich, is an abnormal bird which may or may not fly. The intended model is the first one, since we have no reason to assume that ostriches fly.

Exercise 8.2. Give the models of the program
                likes(peter,S):-student_of(S,peter).
                student_of(paul,peter).

The Herbrand base of this program is

likes(peter,peter) , likes(peter,paul) ,
likes(paul,peter) , likes(paul,paul) ,
student_of(peter,peter) , student_of(peter,paul) ,
student_of(paul,peter) , student_of(paul,paul) }

The atoms student_of(paul,peter) and likes(peter,paul) are true in every model. If the atom student_of(peter,peter) is true, then so is the atom likes(peter,peter) (three possibilities). Disregarding the other four atoms, we obtain the following models:

student_of(paul,peter) , likes(peter,paul)  }

student_of(paul,peter) ,
   
likes(peter,paul) , likes(peter,peter)  }

student_of(paul,peter) , student_of(peter,peter) ,
   
likes(peter,paul) , likes(peter,peter)  }

Taking the four remaining atoms into account, we obtain 3*2 4 =48 models. (See also Exercise 2.6.)

Exercise 8.3. Apply Predicate Completion to the program
                wise(X):-not teacher(X).
                teacher(peter):-wise(peter).

The completion of this program is

X: wise(X) ¬teacher(X)

X: teacher(X) (X=peter wise(peter))

The first formula states that somebody is wise if and only if he is not a teacher; the second formula says that Peter is wise if and only if he is a teacher. Together, these two statements are inconsistent.

C.9  Inductive reasoning

Exercise 9.3. Determine the q -LGG of the following two clauses:
         reverse([2,1],[3],[1,2,3]):-reverse([1],[2,3],[1,2,3])
   reverse([a],[],[a]):-reverse([],[a],[a])

reverse([H|T],A,[RH|RT]):-reverse(T,[H|A],[RH|RT])

This is the recursive clause in the version with accumulator of the reverse/3 predicate (section 3.6), with one small difference: here, the third argument is required to be a non-empty list (which it always is). Notice that this clause is not strictly constrained, and cannot be inferred by the induction programs in sections 9.2 and 9.3 (see als Exercise 9.4).

Simply Logical

Peter Flach,
University of Bristol

Intelligent Reasoning by Example

This book discusses methods to implement intelligent reasoning by means of Prolog programs. The book is written from the shared viewpoints of Computational Logic, which aims at automating various kinds of reasoning, and Artificial Intelligence, which seeks to implement aspects of intelligent behaviour on a computer.

Read more »