Title: Theory / Unimportant / CS / Programming / Prolog (The art of)
Tags: fromMath mathToDef hasNotNewEffectReturnsMeaning fromAlgorithm algorithmWithCardNameButNoFieldName2 fromImplementation récupéré FromInstruction computer_to_instruction some_instruction hasSeenConjDef examplesSwitchExample1 MissingMedia automatedNewLineAfterCommaSpace effectNew effectToImplementation instructionToImplementation mathToSee oldAlgoNewName

Name: Atoms
Definition: Name of individuals.
Page: 11
Chapter: 1
Notation: Start by lower case

Name: Fact
Definition: Simplest kind of statement.
Page: 11
Chapter: 1
Context: Prolog
Name2: Predicate

Name: Query
Definition: A question
Page: 12
Chapter: 1
Section: 2

Name: Goal
Definition: An entity without . or ?
Page: 12
Chapter: 1
Section: 2
Context: Prolog

Name: Identity deduction rule
Definition: From P deduce P
Page: 13
Chapter: 1
Section: 2

Name: Variable
Definition: An element which represents an entity.
Page: 13
Chapter: 1
Section: 2
Denoted by: Element starting with upper case

Name: Term
Definition: Variables
-atoms applied to terms
Page: 13
Chapter: 1
Section: 2

Name: A ground query, goal or term
Definition: A query/goal/term in which no variable occurs.
Page: 14
Chapter: 1
Section: 2

Name: A substitution
Definition: A finite set of pairs of the form \(X_i=t_i\), with \(X_i\ne X_j\) for all \(i\ne j\), and no \(X_i\) occurs in the \(t_j\).
Page: 14
Chapter: 1
Section: 3

Name: An instance of \(b\)
Definition: \(b\theta\) for some substitution \(\theta\).
Page: 14
Chapter: 1
Section: 3
Variables: \(b\) terms

Name: Existential query
Definition: A query with variables
Page: 14
Chapter: 1
Section: 3

Name: Generalization deduction rule
Definition: An existential query \(P\) is a logical consequence of an instance \(P\theta\) of it
Page: 14
Chapter: 1
Section: 3

Name: Universal fact
Definition: A fact with variables
Page: 14
Chapter: 1
Section: 5

Name: Instantation deduction rule
Definition: From a universally quantified statement \(P\), deduce an instance \(P\theta\) of it.
Page: 14
Chapter: 1
Section: 5

Name: A common instance of \(A\) and \(B\)
Definition: \(C\) a term such that \(A=C\theta\) and \(B=C\theta'\) for some substitutions \(\theta,\theta'\).
Page: 16
Chapter: 1
Section: 5
Variables: \(A,B\) terms

Name: An answer to \(q\) using the fact \(f\)
Definition: A common instance of \(f\) and \(q\).
Page: 16
Chapter: 1
Section: 5
Variables: \(f\) a fact and \(q\) a query

Name: Conjonctive query
Definition: A sequence of queries, separated by comma, ending with question mark
Page: 16
Chapter: 1
Section: 6

Name: A solution to \(A_1,\dots,A_n?\)
Definition: A substitution \(\theta\) such that \(A_1\theta,\dots,A_n\theta\) are ground instances of facts in \(P\).
Page: 18
Chapter: 1
Section: 6
Variables: \(A_1,\dots,A_n?\) a conjonctive query and \(P\) a program

Name: Rule
Definition: Statement of the form: \(A\leftarrow B_1,\dots,B_n\)
Page: 18
Chapter: 1
Section: 7

Name: The head of the rule
Definition: \(A\).
Page: 18
Chapter: 1
Section: 7
Variables: \(A\leftarrow B_1,\dots,B_n\) a rule

Name: The body of the rule
Definition: \(B_1,\dots,B_n\).
Page: 18
Chapter: 1
Section: 7
Variables: \(A\leftarrow B_1,\dots,B_n\) a rule

Name: Horn Clause
Definition: Rules
Page: 18
Chapter: 1
Section: 7
Definition2: fact
Conjdef: Either
Definition3: queries
Name2: Clause

Name: Unit clause
Definition: A rule with empty body
Page: 18
Chapter: 1
Section: 7
Name2: Fact

Name: Iterative clause
Definition: A rule with exactly one element in the body
Page: 18
Chapter: 1
Section: 7

Name: Modus Ponens
Definition: From the rule \(R=(A\leftarrow B_1,\dots,B_n)\) and the facts \(B_1',\dots,B_n'\), \(A'\) can be deduced if \(A'\leftarrow B_1',\dots,B'_n\) is an instance of \(R\).
Page: 19
Chapter: 1
Section: 7

Name: Logic program
Definition: A finite set of rules
Page: 19
Chapter: 1
Section: 7

Name: A logical consequence of \(P\)
Definition: there is a clause in \(P\) with ground instances \(A\leftarrow B_1,\dots,B_n\) such that
Page: 20
Chapter: 1
Section: 7
Variables: \(P\) a program
Definition2: the \(B_i\)'s are logical consequences of \(P\) and
Conjdef: An existentially quantified goal \(G\) such that
Definition3: \(A\) is an instance of \(G\)

Name: Resolvent
Definition: A goal at some stage of the computation
Page: 22
Chapter: 1
Section: 8
Variables: \(G\) a goal and \(P\) a program

Name: Trace
Definition: Sequence of resolvents produced during the computation.
Page: 22
Chapter: 1
Section: 8
Variables: \(G\) a goal
\(P\) a program

Name: Reduction of \(G\)
Definition: Replacing of \(G\) by the body of an instance of a clause in \(P\) whose head is identical to the chosen goal.
Page: 23
Chapter: 1
Section: 8
Variables: \(G\) a goal
\(P\) a program

Name: A goal derived from \(G\) in \(P\)
Definition: The result of the effect of a reduction of \(G\) in \(P\).
Page: 23
Chapter: 1
Section: 8
Variables: \(G\) a goal
\(P\) a program
Extra: \(G\) is reduced

Name: Proof tree
Definition: Nodes and edges representing the goals reduced during the computation
Page: 25
Chapter: 1
Section: 8
Variables: \(G\) a goal
\(P\) a program

Name: The meaning of \(P\)
Definition: The set of ground goals deducible from \(P\).
Page: 26
Chapter: 1
Section: 9
Variables: \(P\) a program
Notation: \(M(P)\)

Name: A correct program
Definition: A program \(P\) such that \(M(P)\subseteq M\).
Page: 26
Chapter: 1
Section: 9
Variables: \(M\) an intended meaning
Extra: sound not used in this book

Name: A complete program for \(M\)
Definition: A program \(P\) such that \(M\subseteq M(P)\).
Page: 26
Chapter: 1
Section: 9
Variables: \(M\) an intended meaning

Name: A correct and complete program for \(M\)
Definition: A program \(P\) such that \(M=M(P)\).
Page: 26
Chapter: 1
Section: 9
Variables: \(M\) an intended meaning

Name: A ground goal which is true/false with respect to \(M\)
Definition: A goal \(G\) such that \(G\in M\)/\(G\not\in M\).
Page: 26
Chapter: 1
Section: 9
Variables: \(M\) an intended meaning

Name: Compound term
Definition: function(argument1,argument2).
Page: 13
Chapter: 1
Section: 3

Name: A relation scheme
Definition: A relation which associates to some \(n\)-ary relation symbol a name to each of its \(n\) arguments.
Page: 29
Chapter: 2
Section: 1

Name: Structured data
Definition: The name of a function applied to terms.
Page: 35
Chapter: 2
Section: 1
Example: father(Arthur)

Name: A recursive rule
Definition: A rule defined in function of itself.
Page: 39
Chapter: 2
Section: 3

Page: 42
Implementation: p(X_1,...,X_n) <-r(X_1,...,X_n)
p(X_1,...,X_n) <-s(X_1,...,X_n)
Section: 4
Chapter: 2
Effect: Union of \(r\) and \(s\), r_union_s
Variables: \(r,s\) two \(n\)-ary relations
Language: Prolog

Page: 42
Implementation: p(X_1,...,X_n) <-r(X_1,...,X_n),not s(X_1,...,X_n)
p(X_1,...,X_n) <-s(X_1,...,X_n), not r(X_1,...,X_n)
Section: 4
Chapter: 2
Effect: Set difference of \(r\) and \(s\), r_diff_s
Variables: \(r,s\) two \(n\)-ary relations
Language: Prolog

Page: 42
Implementation: p(X_1,...,X_n,Y1,..., Y_m) <-r(X_1,...,X_n),s(Y_1,...,Y_n)
Section: 4
Chapter: 2
Effect: Cartesian product of \(r\) and \(s\), r_x_s
Variables: \(r,s\) two \(n\)- and \(m\)-ary relations
Language: Prolog

Page: 43
Implementation: p((X_i)_i in N) <-r(X_1,...,X_n)
Section: 4
Chapter: 2
Variables: \(r\) an \(n\)-ary relations and
\(N\) a subset of \(\{1,\dots,n\}\)
Name: \(R_{X_i}\)
Language: Prolog
Returns: The projection of \(r\) to \(N\)

Page: 46
Implementation: -p(0)
-p(s(X)) <- p (X).
Section: 4
Chapter: 3
Effect: Natural number
Language: Prolog

Page: 48
Implementation: -0<=X <- natural_number(X)
-s(X)<= s(Y) <- X<= Y
Section: 4
Chapter: 3
Effect: Order relation on natural numbers
Language: Prolog

Page: 48
Implementation: -R?(0,X,X)<- natural (X)
-R?(s(X),Y,s(Z))<- R?(X,Y,Z)
Section: 4
Chapter: 3
Effect: Addition on naturals
Language: Prolog

Page: 51
Implementation: -p?(0,X,0)<- natural (X)
-p?(s(X),Y,Z)<- p?(X,Y,XY), plus (XY,Y,Z).
Section: 4
Chapter: 3
Effect: Multiplications on naturals
Language: Prolog

Page: 51
Implementation: -R?(s(X),0,0)<- natural (X)
-R?(0,s(X),s(0))<- natural (X)
-R?(s(N),X,Y)<- R?(N,X,Z), times (Z,X,Y).
Section: 4
Chapter: 3
Effect: Exponential on naturals
Language: Prolog

Page: 52
Implementation: -p?(0,s(0))
-p?(s(N),F)<- p?(N,F1), times(s(N),F1,F)
Section: 4
Chapter: 3
Effect: Factorials on naturals
Language: Prolog

Page: 52
Implementation: -p?(N1,N2,N1) <- N1 <= N2
-p?(N1,N2,N2) <- N2 <= N1
Section: 4
Chapter: 3
Effect: Minimum function on naturals
Language: Prolog

Page: 53
Implementation: -p?(X,Y,Z) <- Z<Y, times (Y,Q,QY), plus (QY,Z,X)}},
or
-p?(X,Y,Z)<- X<Y
-p?(X,Y,Z)<- p?(X1,Y,X), p?(X1,Y,Z)
Section: 4
Chapter: 3
Effect: Mod on naturals
Language: Prolog

Page: 58
Implementation: -p?(X,[X|Xs])
-p?(X,[Y|Xs])<- p?(X,Xs)
Section: 4
Chapter: 3
Effect: List membership relation
Language: Prolog

Page: 59
Implementation: -p?([ ],Ys)
-p?([X|Xs],[X|Ys])<- p?(Xs,Ys)
Section: 4
Chapter: 3
Effect: List prefix relation
Language: Prolog

Page: 59
Implementation: -p?(Xs,Xs)
-p?(Xs,[X|Ys])<- p?(Xs,Ys)
Section: 4
Chapter: 3
Effect: List suffix relation
Language: Prolog

Page: 62
Implementation: -p?(Xs,Ys)<- p? (Xs,[ ], Ys)
-p?([X|Xs],Acc,Ys)<-p? (Xs,[X|Acc], Ys)
-p?([ ],Ys, Ys).
Section: 4
Chapter: 3
Effect: Reversing a list
Language: Prolog

Page: 60, 109
Implementation: -p?([ ],Ys, Ys)
-p?([X|Xs], Ys, [X|Zs]) <-p?(Xs,Ys,Zs).
Section: 4
Chapter: 3
Effect: Appending two lists
Language: Prolog
Time complexity: quadratic
Linear when unification is done without occur check

Page: 62
Implementation: -p? (X,Y,Zs) <- append (As, [X,Y|Ys],Zs)
Section: 4
Chapter: 3
Effect: Stating that two elements X, Y are adjacent in Zs
Language: Prolog

Page: 62
Implementation: - p?(X,Xs) <- append (As, [X],Xs)
Section: 4
Chapter: 3
Effect: Stating that X is the last element of \(Xs\)
Language: Prolog

Name: A tree which satisfy the heap property
Definition: A tree such that the value at the root is at least as large as the value at his childrens.
Page: 75
Chapter: 3
Section: 4

Name: A Heap
Definition: A tree which satisfies the heap property.
Page: 75
Chapter: 3
Section: 4

Page: 74
Implementation: p(void)
p(tree(Element, Left, Right)) <- p(Left),p(Right)
Section: 4
Chapter: 3
Effect: Definining the set of binary tree, binary_tree
Language: Prolog

Page: 74
Implementation: p(X,tree(X,Left,Right)).
p(X,tree(Y,Left,Right)) <- p (X,Left).
p(X,tree(Y,Left,Right)) <- p (X,Right).
Section: 4
Chapter: 3
Effect: Determining whether X belongs to the tree in the second argument, tree_member
Language: Prolog

Page: 75
Implementation: p(void, void).
p(tree(X,Left1,Right1), tree(X,Left2,Right2)) <- p(Left1,Left2), p(Right1,Right2).
p(tree(X,Left1,Right1), tree(X,Left2,Right2)) <- p(Left1,Right2), p(Right1,Left2).
Section: 4
Chapter: 3
Effect: Isomorphism of binary tree
Language: Prolog

Name: Its preorder traversal
Definition: The element at the root, followed by the traversal of its left subtree and then by the traversing of its right subtree.
Page: 75
Chapter: 3
Section: 4
Variables: \(T\) a tree

Name: Its postorder traversal
Definition: The traversal of its left subtree, followed by the traversing of its right subtree and then its element at the roots.
Page: 75
Chapter: 3
Section: 4
Variables: \(T\) a tree

Name: Its inorder traversal
Definition: The traversal of its left subtree, followed by the element at the root, and finally the traversing of its right subtree.
Page: 75
Chapter: 3
Section: 4
Variables: \(T\) a tree

Name: \(s\) is more general than \(t\)
Definition: \(t\) is an instance of \(s\) and \(s\) is not an instance of \(t\).
Page: 88
Chapter: 4
Section: 1
Variables: \(s,t\) terms

Name: \(s\) is an alphabetic variant of \(t\)
Definition: \(t\) is an instance of \(s\) and \(s\) is an instance of \(t\).
Page: 88
Chapter: 4
Section: 1
Variables: \(s,t\) terms

Name: An unifier of \(s\) and \(t\)
Definition: A substitution which makes \(s\) and \(t\) identical.
Page: 88
Chapter: 4
Section: 1
Variables: \(s,t\) terms

Name: A most general unifier of \(s\) and \(t\)
Definition: A unifier of \(s\) and \(t\) such that the associated common instance is most general.
Page: 88
Chapter: 4
Section: 1
Variables: \(s,t\) terms
Abbreviation: mgu

Page: 90
Implementation: \(U=\{\{s,t\}\}\)// a set of pair of terms to unify, initialized with \(\{s,t\}\).
\(S=\emptyset\)//A substitution.
Pop \(\{s,t\}\in U\):
-If both are distinct:
--If \(s\) is a variable and \(t\) does not contain \(s\):
---add \((s, t)\) in \(S\)
---replace \(s\) by \(t\) in every right element of \(S\).
--If \(s=f(s_1,\dots,s_n)\) and \(t=f(t_1,\dots,t_n)\):
---add each \(\{s_i,t_i\}\) to \(u\).
--Else reject.
Section: 1
Chapter: 4
Effect: Unification of two terms \(s\) and \(t\)
Variables: \(s,t\) terms
Context: Prolog

Name: A computation of \(Q\) by \(P\)
Definition: \(Q_i\) is a conjunctive goal
Page: 92
Chapter: 4
Section: 2
Variables: \(Q\) a goal,
\(P\) a program
Definition2: \(G_i\) is a goal occuring in \(Q_i\)
Conjdef: A (possibly infinite) sequence of triples \(\langle Q_i,G_i,C_i\rangle\)
Definition3: \(C_i\) is a clause \(A\leftarrow B_1,\dots,B_k\) in \(P\), renamed so that it contains new variable symbols not occuring in \(Q_j\), \(0\le j\le i\).
Definition4: \(Q_{i+1}\) is either:
Definition5: the result of replacing \(G_i\) by the body of \(C_i\) in \(Q_i\), and applying the substitution \(\theta_i\), the mgu of \(G_i\) and \(A_i\)
Definition6: the constant true in \(G_i\) is the only goal in \(Q_i\) and the body of \(C_i\) is empty
Definition7: the constant fail if \(G_i\) and the head of \(C_i\) do not unify.

Name: A goal derived from \(G_j\) and \(C_j\)
Definition: \(i\ge j\)
Page: 92
Chapter: 4
Section: 2
Variables: \(Q\) a goal,
\(P\) a program,
\(\langle Q_i,G_i,C_i\rangle\) a computation of \(Q\) by \(P\)
\(j\) an index of the sequence
Definition2: where \(C_i=A_i\leftarrow B_{i1},\dots, B_{ik_i}\)
Conjdef: A goal \(B_{ij}\theta_i\) with
Definition3: \(\theta_i\) is the mgu of \(G_i\) and \(A_i\)

Name: A goal invoked by \(G_i\) and \(C_i\)
Definition: \(B_{ik}\) occurs in the body of clause \(C_i\) (i.e. \(C_i=A_i\leftarrow B_{i1},\dots, B_{ik_i}\))
Page: 92
Chapter: 4
Section: 2
Variables: \(Q\) a goal,
\(P\) a program,
\(\langle Q_i,G_i,C_i\rangle\) a computation of \(Q\) by \(P\)
\(i\) an index of the sequence
Definition2: \(\theta_i\) is the mgu of \(G_i\) and \(A_i\)
Conjdef: A goal \(G_j=B_{ik}\theta_i\) where

Name: A parent of a goal \(G_i\)
Definition: A goal \(G_j\) such that \(G_i\) is derived from \(G_j\).
Page: 92
Chapter: 4
Section: 2
Variables: \(Q\) a goal,
\(P\) a program,
\(\langle Q_i,G_i,C_i\rangle\) a computation of \(Q\) by \(P\),
\(i\in\mathbb N\)

Name: Sibling goals
Definition: Two goals with the same parent.
Page: 92
Chapter: 4
Section: 2
Variables: \(Q\) a goal,
\(P\) a program,
\(\langle Q_i,G_i,C_i\rangle\) a computation of \(Q\) by \(P\)

Name: The trace of the computation
Definition: The sequence \(\langle G_i,\theta'_i\rangle\) where \(\theta'_i\) is the subset of the mgu \(\theta_i\) computed at the \(i\)-th reduction, restricted to variables in \(G_i\).
Page: 92
Chapter: 4
Section: 2
Variables: \(Q\) a goal,
\(P\) a program,
\(\langle Q_i,G_i,C_i\rangle\) a computation of \(Q\) by \(P\)

Name: A solution to the query
Definition: An instance of the query for which a proof is found.
Page: 93
Chapter: 4
Section: 2
Variables: \(Q\) a goal,
\(P\) a program,

Name: An interpreter
Definition: A program taking as input a goal, a program, and computing a solution to the goal using this program, or «no» if no such solution exists.
Page: 22, 92
Chapter: 1, 4
Section: 8, 2
Context: Prolog

Name: A scheduling policy
Definition: A program, which, given a finite computation \(\langle Q_i,G_i,C_i\rangle\) of \(Q\) by \(P\), choose which goals to add and to remove.
Page: 93
Chapter: 4
Section: 2
Variables: \(Q\) a goal,
\(P\) a program
Context: computation

Name: Its operational semantic
Definition: A way of describing procedurally the meaning of a program.
Page: 102
Chapter: 5
Section: 1
Variables: \(P\) a program

Q: The Herbrand [...] is finite implies the Herbrand [...] is finite.
A: universe; base
Page: 103
Chapter: 5
Section: 1
Variables: \(P\) a logic program

Name: An interpretation for \(P\)
Definition: A subset of the Herbrand base.
Page: 103
Chapter: 5
Section: 1
Variables: \(P\) a logic program

Name: A model for \(P\)
Definition: for each ground instance of a clause in the program \(A\leftarrow B_1,\dots,B_n\), \(A\) is in \(I\) if \(B_1\dots,B_n\) are in \(I\).
Page: 104, 105
Chapter: 5
Section: 1
Variables: \(P\) a logic program,
Definition2: \(T_p(I)=I\)
Conjdef: An interpretation \(I\) such that

Name: The minimal model
Definition: The intersection of the models of \(P\)
Page: 104
Chapter: 5
Section: 1
Variables: \(P\) a logic program
Name2: The declarative meaning of \(P\)
Abbreviation: \(M(P)\)
Name3: The meaning of \(P\)

Name: Denotational semantic
Definition: associating with the program a function over the domain computed by the program
Page: 105
Chapter: 5
Section: 1
Conjdef: Something which assigns meanings to programs based on

Question: The domain of computations of \(P\)
Answer: the set interpretations for \(P\)
Page: 105
Chapter: 5
Section: 1
Variables: \(P\) a logic program

Definition: \(A\leftarrow B_1,\dots,B_n,n\ge 0\) is a ground instance of a clause in \(P\)
Page: 105
Chapter: 5
Section: 1
Variables: \(P\) a logic program
\(I\) an interpretation for \(P\)
Notation: \(T_p(I)\)
Definition2: \(B_1,\dots,B_n\in I\)
Conjdef: the set of \(A\in B(P)\) such that

Name: Natural mapping
Definition: Sends [$]\defFun{\text{Interpretation}}{\text{Interpretation}}{I}{T_P(I)}[/$]
Page: 105
Chapter: 5
Section: 1
Variables: \(P\) a logic program
Notation: \(T_p\)
Typ: Monotonic map

Name: A domain
Definition: A set of goals, not necessarily ground, closed under the instance relation
Page: 105
Chapter: 5
Section: 1

Name: A termination domain
Definition: every computation of \(P\) on every goal in \(D\) terminates.
Page: 106
Chapter: 5
Section: 1
Variables: \(P\) a program
Example: for append: the set of goals where the first and/or the third argument is a complete list.
Conjdef: A domain \(D\) such that

Name: A complete type
Definition: A set closed under the instance relation.
Page: 107
Chapter: 5
Section: 1
Example: for natural numbers: the terms of the form \(s^n(0)\) for \(n\in\mathbb N\) ???

Name: The incomplete type
Definition: The set of terms that have instances in \(T\) and instances not in \(T\)
Page: 107
Chapter: 5
Section: 1
Variables: \(T\) a complete type
Context: prolog
Notation: \(IT\)
Example: the terms of the form \(s^n(X)\) for \(n\in\mathbb N\) ????
Applied to: natural numbers

Name: A complete list
Definition: A list whose instance satisfies the definition
list ([ ]).
list([X|Xs]) <- list(Xs).
Page: 107
Chapter: 5
Section: 1
Kind: Def
Example: [a,b,c]
Example2: [a,X,b]

Name: An incomplete list
Definition: A list whose some instance satisfies the definition
list ([ ]).
list([X|Xs]) <- list(Xs).
and some instance does not
Page: 107
Chapter: 5
Section: 1
Kind: Def
Example: X
Example2: [a,b|Xs]

Instruction: pred(atom1,atom2).
Page: 11
Effect: The fact that the predicate pred holds on the pair atom1 atom2
Language: Prolog
Chapter: 1

Instruction: predName(atom_1,atom_2)?
Page: 12
Effect: Asking whether the predicate predName holds on the pair atom_1 atom_2
Language: Prolog
Chapter: 1
Section: 2

Instruction: [ ]
Page: 56
Effect: The empty list
Language: Prolog
Chapter: 2
Section: 4

Instruction: [X|Y]
Page: 56
Effect: The list with head X and tail Y
Language: Prolog
Chapter: 2
Section: 4

Instruction: [a,b,c]
Page: 56
Effect: The list with the three elements a, b, c
Language: Prolog
Chapter: 2
Section: 4

Instruction: void
Page: 72
Effect: The empty binary tree
Language: Prolog
Chapter: 3
Section: 4

Instruction: tree(
  Element,
  Left,
  Right
)
Page: 72
Effect: The binary tree with root Element, Left and Right subtree
Language: Prolog
Chapter: 3
Section: 4

Name: The Herbrand universe of \(P\)
Definition: The set of all ground terms that can be formed from the constants and function symbols appearing in \(P\).
Page: 102
Chapter: 5
Section: 1
Variables: \(P\) a logic program
Notation: \(U(P)\)

Smaller0: there are no constant symbol or no function symbols
Greater0: finite
Page: 102
Chapter: 5
Section: 1
Variables: \(P\) a logic program
Smaller to greater: iff
Prefix Greater: the Herbrand universe is

Name: Its Herbrand base
Definition: The set of all ground goals that can be formed from the predicates in \(P\) and the terms in the Herband universe.
Page: 102
Chapter: 5
Section: 1
Variables: \(P\) a logic program
Notation: \(B(P)\)

Name: the size of \(t\)
Definition: The number of symbols in the textual representation of \(t\)
Page: 108
Chapter: 5
Section: 3
Variables: \(t\) a term

Name: The length complexity of \(P\)
Definition: A function \(L:\mathbb N\to\mathbb N\) such that, for any goal \(G\in M\) of size \(n\), there is a proof of \(G\) with respect to \(P\) of length less than \(L(n)\)
Page: 108
Chapter: 5
Section: 3
Variables: \(P\) a program,
\(M\) a meaning
Notation: \(L(n)\)

Name: The goal-size complexity of \(P\)
Definition: A function \(f:\mathbb{N\to N}\) such that, for any goal \(A\in M\) of size \(n\) there is a proof of \(A\) with respect to \(P\) of goal-size at most \(f(n)\)
Page: 109
Chapter: 5
Section: 3
Variables: \(P\) a program,
\(M\) a meaning
Notation: \(G(n)\)

Name: The depth complexity of \(P\)
Definition: A function \(f:\mathbb{N\to N}\) such that, for any goal \(A\in M\) of size \(n\) there is a proof of \(A\) with respect to \(P\) of depth at most \(f(n)\)
Page: 109
Chapter: 5
Section: 3
Variables: \(P\) a program,
\(M\) a meaning
Notation: \(D(n)\)
Kind: def

Name: The depth of \(R\)
Definition: the deepest invocation of a goal in the associated reduction
Page: 109
Chapter: 5
Section: 3
Variables: \(P\) a program,
\(M\) a meaning
\(R\) a proof

Name: The goal-size of \(R\)
Definition: the maximum size of any goal reduced
Page: 109
Chapter: 5
Section: 3
Variables: \(P\) a program,
\(M\) a meaning
\(R\) a proof

Name: A search tree
Definition: root \(G\)
Page: 110, 115
Chapter: 5
Section: 4
Variables: \(P\) a program,
\(G\) a goal
Context: Prolog
Definition2: nodes: (possibly conjunctive) goals, with one goal selected
Conjdef: A tree
Definition3: An edge leading from a node \(N\) for each clause in the program whose head unifies with the selected goal
Name2: SLD tree
Definition4: edges' label: substitution applied to the selected goal
Definition5: success node: leaf with empty goal
Definition6: failure node: leaf with non-empty irreduccible goal
Representation: leftmost goal is the selected one
Applied to3: The set of computations, where equal part are put in common

Name: A search tree with multiple success node
Page: 112
Chapter: 5
Section: 4
Variables: \(P\) a program,
\(G\) a goal

Definition: A relation which holds only if \(G\) belongs to the finite failure set.
Page: 114
Chapter: 5
Variables: \(P\) a program,
\(G\) a goal
Notation: not \(G\)

Name: A finitely failed search tree
Definition: A search tree without infinite branch nor success node
Page: 114
Chapter: 5

Name: The finite failure set of \(P\)
Definition: The set of goals \(G\) such that \(G\) has a finitely failed search tree with respect to \(P\)
Page: 114
Chapter: 5
Variables: \(P\) a program,
Context: Prolog

Page: 114
Section: 5
Example: p?(Xs,Ys) <- not (member (X,Xs), member (X,Ys))
Assuming: disjoint

Name: Selecting a literal, using a Linear strategy, restricted to Definite clauses
Page: 115
Chapter: 5
Abbreviation: SLD