# Glossary

# 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¶
- 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).
```

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

- ground term/atom/clause¶
- head¶
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 form – predicate 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