# Glossary¶

Tip

This glossary is a work in progress. It will contain a mixture of brief definitional entries and short essays complementing the material covered in the main text. Eventually, the online book and glossary can be seen as an updated, revised and extended second edition.

atom

An atom has the form pred(t1,...,tn), where pred is a predicate and t1,...,tn are terms. n is the arity of the predicate. Predicates with different arities are treated as different even if they use the same token. A 0-arity predicate is also called a proposition.

body

TO DO

clause

A clause has the form head :- body, to be read head IF body or IF body THEN head. The head is a disjunction of atoms separated by semicolons. The body is a conjunction of atoms separated by commas.

Special cases: body can be empty, in which case the clause is written as either head or as head :- true. Similarly, head can be empty, in which case the clause is written as either :-body or as false :- body. The empty clause, written as false :- true or as [], indicates a logical contradiction.

In Prolog, clause heads must have a single atom (definite clause). Clauses with an empty head are interpreted as queries.

completeness

TO DO

conjunctive normal form

TO DO

constant

TO DO

counter-example

TO DO

decidable

TO DO

declarative semantics

TO DO

definite clause

A clause with a single atom in the head.

existential variable

TO DO

failure-driven loop

TO DO

functor

TO DO

general clause

TO DO

generate and test

A typical Prolog backtracking search strategy, where a generator predicate produces potential solutions and a tester checks whether all requirements are satisfied. Below are a few classic AI examples of blind generate and test, where all checking is done in the tester. The search will be more efficient if some requirements are checked in the generator.

/*
* Find unique assignments of decimal digits to letters
* such that the sum is correct.
*
*     S E N D
*     M O R E
*     ------- +
*   M O N E Y
*/

% Easy one: 8 letters, plenty of solutions
sum1(Sum):-
Sum=([S,E,N,D]+[M,O,R,E]=[M,O,N,E,Y]),
gentest([S,E,N,D,M,O,R,Y],Sum).

/*
*     C R O S S
*     R O A D S
*     --------- +
*   D A N G E R
*/

% Harder one: 9 letters, only one solution
sum2(Sum):-
Sum=([C,R,O,S,S]+[R,O,A,D,S]=[D,A,N,G,E,R]),
gentest([C,R,O,S,A,D,N,G,E],Sum).

% Blind generate-and-test approach
gentest(Letters,Sum):-
generate(Letters),
test(Sum).

generate(Letters):-
generate(Letters,[0,1,2,3,4,5,6,7,8,9]).

generate([],_).
generate([L|Ls],Digits):-
remove_one(L,Digits,LessDigits),
generate(Ls,LessDigits).

test(Word1+Word2=Word3):-
calc(Word1,0,N1),
calc(Word2,0,N2),
calc(Word3,0,N3),
N3 is N1+N2.

calc([],N,N).
calc([H|T],N0,N):-
N1 is 10*N0+H,
calc(T,N1,N).

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

/** <examples>
?- sum1(Sum).
?- sum2(Sum).
*/

% :-use_rendering(chess). % Uncomment this line for chess renderer

%%% Place N queens on an N-by-N chess board such that none of them are attacked
%%% Columns are listed in the order row 1, row 2, ..., row 8
nqueens(N,Columns) :-
setof(X,between(1,N,X),Rows),
permute(Rows,Columns), % generator
test(Columns).         % tester

%%% blind generator: permute rows
permute([],[]).
permute(L,[X|PR]):-
remove_one(X,L,R),
permute(R,PR).

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

%%% tester
test([]).
test([Column|Columns]) :-
noattack(Column,Columns,1),
test(Columns).

noattack(_,[],_).
noattack(Y,[Y1|Ylist],Xdist) :-
abs(Y-Y1) =\= Xdist,
Xdist1 is Xdist+1,
noattack(Y,Ylist,Xdist1).

/** <examples>
?- nqueens(8,Columns).
*/

ground term/atom/clause

A term, atom or clause without variables.

TO DO

Herbrand universe

The set of all ground terms. These represent all the “things” you can talk about. The Herbrand universe is infinite if we have one or more functors, finite otherwise (i.e., in propositional and relational clausal logic).

Herbrand base

The set of all ground atoms. These represent statements that can be true or false. Finite or infinite depending on the Herbrand universe.

Herbrand interpretation

assignment of truth values true/false to all ground atoms in the Herbrand base. Usually represented by the subset of true atoms. Each Herbrand interpretation represents a possible state of affairs in the world (possible world).

inference rule

TO DO

list

TO DO

literal

Given a clause, an atom is a positive/negative literal if it occurs in the body/head. This corresponds to the interpretation of a clause h1 ; h2 :- b1 , b2 as a disjunction $$h1 \lor h2 \lor \neg b1 \lor \neg b2$$, in which head literals occur unnegated and body literals occur negated.

logical consequence

A clause $$C$$ is a logical consequence of a program $$P$$ (or $$P$$ entails $$C$$) iff every model of $$P$$ is also a model of $$C$$; we write $$P \models C$$. If this isn’t the case (i.e., some model of $$P$$ is not a model of $$C$$), then $$C$$ expresses some knowledge that is not contained in $$P$$.

Edge cases: any tautology such as a :- a is a logical consequence of any program; an inconsistent program (e.g., containing both a and :-a) has no models and hence entails anything.

meta-interpreter

TO DO

meta-level

TO DO

minimal model

TO DO

model

A Herbrand interpretation that makes a clause or program true. A ground clause is false in an interpretation if all body atoms are true and all head atoms are false (counter-example), and true otherwise. A non-ground clause is true iff all its ground instances over the Herbrand universe are. A program is true if all of its clauses are.

most general unifier

TO DO

negation as failure

TO DO

object-level

TO DO

possible world

TO DO

predicate

TO DO

predicate logic

TO DO

procedural semantics

TO DO

program

A (logic) program consists of one of more clauses, read conjunctively. Hence a program is said to be in conjunctive normal form, i.e., a conjunction of disjunctions of (possibly negated) atoms. Normal forms limit the number of ways programs can be written, which is computationally advantageous.

proof by refutation

A proof by refutation, also referred to as reduction to the absurd, adds the negation of the query (what you want to prove) to the program, and then uses resolution to derive the empty clause (falsity). If that succeeds, then the original (un-negated) query is a logical consequence of the program – but only under the substitutions needed for all resolution steps.

proof tree

TO DO

proposition

TO DO

propositional clausal logic

TO DO

query

TO DO

recursion

TO DO

relational clausal logic

TO DO

resolution

The single inference rule in clausal logic is resolution. (This is a consequence of having a normal formpredicate logic needs many more inference rules.) Resolution takes two clauses and infers a third clause that is a logical consequence (i.e., resolution is *sound). We can chain several resolution steps together into a proof to produce further logical consequences.

In propositional clausal logic, resolution is applicable to any two clauses where the same literal occurs positively in one clause (i.e., in the head) and negatively in the other (in the body). This literal is “resolved away”, and the remaining literals are combined in the inferred clause, keeping their sign (location in head or body). It follows that if the two input clauses are definite, then so is the inferred clause.

With variables we first may have to apply a substitution to make the positive/negative literal pair identical. Such a substitution is called a unifier; it is applied to the entire clause and carried along to the rest of the proof. Applying a substitution to a clause produces a logical consequence, so this doesn’t affect the soundness of resolution. We are generally only interested in most general unifiers that don’t make unnecessary substitutions.

Resolution cannot infer all logical consequences (e.g., arbitrary tautologies) and hence is incomplete}. This can be overcome by turning things around, starting from the thing you want to prove. Technically, this is realised by proof by refutation.

refutation

TO DO

refutation-complete

TO DO

soundness

TO DO

stratified program

TO DO

substitution

TO DO

success set

TO DO

tautology

TO DO

term

A term is either a variable or has the form f(t1,...,tn), where f is a functor and t1,...,tn are terms. n is the arity of the functor. Variable tokens start with an uppercase letter; functor tokens start with a lowercase letter. A 0-arity functor is also called a constant.

unification

TO DO

unifier

TO DO

variable

TO DO