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

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.

*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.

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

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.

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).

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

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.

*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]).

*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 ‘ **if** … **then** …’ 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*) 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

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.

*Exercise 3.2.* Draw the SLD-tree for the following program:

`list([]).
list([H|T]):-list(T).`

and the query

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 {

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

*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

*Exercise 3.7.* Given the program

`p:-q,r,s,!,t.
p:-q,r,u.
q.
r.
u.` show that the query

*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

*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

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

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.

The exercises in this chapter should not provide major difficulties.

*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

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).

*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).

*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].

*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.

*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).

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.