Title: Theory / Important / CS / Algo / Artificial intelligence / Introduction{ / 3 Knowledge
Tags: fromMath mathToDef hasNotNewEffectReturnsMeaning FromInstruction computer_to_instruction fromAlgorithm oldAlgoNewName algoToProg mathToSee some_instruction examplesSwitchExample1 EquivalentButNoIntermediate addIntermediateCard automatedNewLineAfterCommaSpace effectToImplementation hasSeenConjDef seen_description similarity toProgram

Name: Knowledge base
Definition: A set of sentences in knowledge representation language
Page: 238
Chapter: 7
Abbreviation: KB

Name: Axiom
Definition: A sentence which is not derived from other sentences.
Page: 238
Chapter: 7
Context: Knowledge base

Name: Inference
Definition: Deriving new sentences from old ones.
Page: 238
Chapter: 7
Variables: \(K\) a Knowledge base

Name: Background knowledge
Definition: Sentences in \(K\) at initialization.
Page: 238
Chapter: 7
Variables: \(K\) a Knowledge base

Question: When an agent is called:
-
Answer: Tell the percept, Ask action, Tell which action is performed.
Page: 239
Chapter: 7
Variables: \(K\) a KB

Name: Knowledge level
Definition: What the agent knows and what its goals are.
Page: 240
Chapter: 7
Section: 1
Context: knowledge-based agent

Name: Implementation level
Definition: How to represent knowledge and reasoning about it.
Page: 239
Chapter: 7
Section: 1

Name: Declarative approach of KB
Definition: States how the wold works, fact by fact until the agent knows how to operate in the world.
Page: 240
Chapter: 7
Section: 1

Name: Procedural approach of KB
Definition: Encode desired behaviors directly as program code.
Page: 240
Chapter: 7
Section: 1
Context: Knowledge Base

Name: Syntax
Definition: Specification of which sentences are well formed.
Page: 244
Chapter: 7
Section: 3

Name: Semantics
Definition: Meaning of sentences
Page: 244
Chapter: 7
Section: 3
Definition2: the truth of each sentence with respect to each possible world.
Conjdef: Either

Name: Possible world
Definition: An assignation of variable to values.
Page: 244
Chapter: 7
Section: 3
Context: Knowledge in AI
Name2: Model

Name: \(m\) satisfies \(\alpha\)
Definition: \(\alpha\) is true in model \(m\).
Page: 244
Chapter: 7
Section: 3
Variables: \(\alpha\) a formula
\(m\) a model
Name2: \(m\) is a model of \(\alpha\)

Name: \(\alpha\) entails \(\beta\)
Definition: \(\beta\) holds in every models where \(\alpha\) holds.
Page: 245
Chapter: 7
Section: 3
Variables: \(\alpha,\beta\) formulas
Notation: \(\alpha\models\beta\)

Name: Model checking
Definition: Given a KB and a sentence \(\alpha\), checks every models permited by the KB to check whether \(\alpha\) holds.
Page: 245
Chapter: 7
Section: 3

Definition: \(\alpha\) is derived from KB by \(i\).
Page: 246
Chapter: 7
Section: 3
Variables: KB,
\(\alpha\) a sentence
Notation: \(KB\vdash_i\alpha\)

Name: Sound inference
Definition: An inference which derives only entailed sentences.
Page: 246
Chapter: 7
Section: 3

Name: Complete inference algorithm
Definition: An inference algorith which derives every entailed sentences.
Page: 246
Chapter: 7
Section: 3

Name: An atomic sentence
Definition: A sentence which is a single proposition symbol.
Page: 246
Chapter: 7
Section: 4.1

Name: A positive litteral
Definition: A litteral which is composed only of an atomic sentence without negations.
Page: 248
Chapter: 7
Section: 4.1

Name: A negative litteral
Definition: The negation of an atomic sentence.
Page: 248
Chapter: 7
Section: 4.1

Name: A conjunct of \(C_1\land C_2\)
Definition: \(C_i\).
Page: 248
Chapter: 7
Section: 4.1
Variables: \(C_1\land C_2\) a sentence

Name: A disjunct
Definition: \(C_i\).
Page: 248
Chapter: 7
Section: 4.1
Variables: \(C_1\lor C_2\) a sentence

Name: Premise
Definition: \(C_1\).
Page: 248
Chapter: 7
Section: 4.1
Variables: \(C_1\implies C_2\) a sentence
Name2: Antecedent

Name: Conclusion
Definition: \(C_2\).
Page: 248
Chapter: 7
Section: 4.1
Variables: \(C_1\implies C_2\) a sentence
Name2: Consequent

Name: An implication
Definition: A statement of the form \(A\implies B\).
Page: 248
Chapter: 7
Section: 4.1
Name2: -implies statement

Name: A disjunction
Definition: A statement of the form \(A\lor B\).
Page: 248
Chapter: 7
Section: 4.1

Name: A conjunction
Definition: A statement of the form \(A\land B\).
Page: 248
Chapter: 7
Section: 4.1

Name: A negation
Definition: A statement of the form \(\neg B\).
Page: 248
Chapter: 7
Section: 4.1

Name: Its truth value in \(m\)
Definition: If \(S\) is true, then: true
Page: 249
Chapter: 7
Section: 4.2
Variables: \(S\) a sentence
\(m\) a model
Definition2: If \(S\) is an atomic formula, then the value of \(S\) in \(m\),
Definition3: if \(S=\neg P\), then false if \(P\) is true, otherwise true in \(m\)
Definition4: if \(S=P\lor Q\), then true if \(P\) or \(Q\) is false in \(m\)
Definition5: if \(S=P\land Q\), then true if \(P\) and \(Q\) are true in \(m\)
Definition6: if \(S=P\implies Q\) then true if \(P\) is false or \(Q\) true in \(m\)
Definition7: if \(S=P\iff Q\) then true if \(P\) and \(Q\) are both true or both false in \(m\).

Name: Its truth table
Definition: A table giving, for each possible world, the truth value of \(S\).
Page: 250
Chapter: 7
Section: 4.1
Variables: \(S\) a sentence

Question: Model checking algorithm to decide whether \(K\) entails \(\alpha\):
-
Answer: list the variables of \(K\) and \(\alpha\). Loop for each truth assignation. If one assignation holds for \(K\) and not for \(\alpha\) return false. Otherwise return true.
Page: 251
Chapter: 7
Section: 4.4
Variables: \(K\) a knowledge base, \(\alpha\) a propositional sentence

Name: Logically equivalent sentences
Definition: Sentences which are true in the same models.
Page: 253
Chapter: 7
Section: 4.4

Name: Valid sentence
Definition: A sentence which is valid in all models.
Page: 254
Chapter: 7
Section: 5
Name2: Tautologies

Name: Satisfiable sentence
Definition: A sentence which is valid in some model.
Page: 254
Chapter: 7
Section: 4.4

Smaller0: \(\alpha\models\beta\)
Greater0: \(\alpha\implies\beta\) is valid
Page: 254
Chapter: 7
Section: 5
Variables: \(\alpha,\beta\) sentences
Smaller to greater: iff
Intermediate: \(\alpha\land\neg\beta\) is unsatisfiable

Name: Modus ponens
Definition: [latex]
\begin{prooftree}
\AxiomC{$\alpha\implies \beta$}
\AxiomC{$\alpha$}
\BinaryInfC{$\beta$}
\end{prooftree}
[/latex]
Page: 254
Chapter: 7
Section: 5.1
Variables: \(\alpha,\beta\) sentences

Name: And-elimination
Definition: [latex]
\begin{prooftree}
\AxiomC{$\alpha\land \beta$}
\UnaryInfC{$\beta$}
\end{prooftree}
[/latex]
Page: 255
Chapter: 7
Section: 5.1
Variables: \(\alpha,\beta\) sentences

Name: The search problem of proving \(\alpha\)
Definition: -Initial state: \(K\),
Page: 251
Chapter: 7
Section: 5.1
Variables: \(\alpha\) sentences,
\(K\) a KB
Definition2: -Actions: inference rule applied to a sentence that match its hypothesis,
Definition3: -Result: add to \(K\) the result of the inference rule,
Extra: top ?
Definition4: -goal: a state that contains \(\alpha\).

Smaller0: \(K\models\alpha\)
Greater0: \(K\land\beta\models\alpha\)
Page: 256
Chapter: 7
Section: 5.1
Variables: \(K\) a KB
\(\alpha,\beta\) sentences
Name: Monoticity
Hide sides: yes

Q: [...]
A: [latex]
\begin{prooftree}
\AxiomC{$l_1\lor \dots\lor l_k$}
\AxiomC{$\neg l_k\lor m_1\lor \dots\lor m_{k'}$}
\BinaryInfC{$l_1\lor\dots\lor l_{k-1}\lor m_1\lor m_{k'}$}
\end{prooftree}.
[/latex]
Page: 257
Chapter: 7
Section: 5.1
Name: Resolution rule

Name: Conjunctive normal form
Definition: A conjunction of disjunction of litterals.
Page: 257
Chapter: 7
Section: 5.1
Abbreviation: CNF

Page: 258
Implementation: tries to refute \(\alpha\land\neg\beta\), as follows:
-transform it in CNF,
-use resolution rule to generate as many disjunction as possible
-if the empty disjunction is found, return true
-otherwise, if no more disjunctions can be created, return false.
Section: 5.1
Chapter: 7
Variables: \(\alpha,\beta\) sentences
Name: Resolution algorithm
Returns: proof that \(\alpha\models\beta\)

Name: A clause
Definition: A disjunction of literals.
Page: 260
Chapter: 7
Section: 5.1

Name: Definite clause
Definition: A disjunction of literals, with exactly one positive litteral.
Page: 261
Chapter: 7
Section: 5.3

Name: Horn clause
Definition: A disjunction of literals, with at most one positive litteral.
Page: 261
Chapter: 7
Section: 5.3

Name: Goal clause
Definition: A disjunction of negative literals.
Page: 261
Chapter: 7
Section: 5.3
Context: Predicate logic

Name: A fact
Definition: A clause composed of a single positive literals.
Page: 261
Chapter: 7
Section: 5.3

Name: The head of \(H\)
Definition: \(y\).
Page: 261
Chapter: 7
Section: 5.3
Variables: \(H=(\neg x_1\lor\dots\lor \neg x_n\lor y) \) a Horn-clause

Name: The body of the clause
Definition: \(x_1\land\dots\land x_n\).
Page: 261
Chapter: 7
Section: 5.3
Variables: \((\neg x_1\lor\dots\lor \neg x_n\lor y)\) a Horn-clause

Page: 264
Implementation: If in \(K\) there is a clause \(\neg x_1\lor\dots\lor\neg x_n\lor\alpha\), try to prove each \(x_i\).
Section: 5.4
Chapter: 7
Variables: \(K\) a KB of definite clause
\(\alpha\) a sentence to prove
Name: Backward chaining algorithm
Time complexity: linear
Returns: A proof of \(\alpha\) if it exists
Name2: Goal directed reasoning

Name: A pure symbol
Definition: A symbol that always appears with the same sign.
Page: 265
Chapter: 7
Section: 6
Variables: \(\bigwedge_i \bigvee_j l_{i,j}\) with the \(l_{i,j}\) literals.

Name: An impure symbol
Definition: A symbol which is not pure.
Page: 265
Chapter: 7
Section: 6
Variables: \(\bigwedge_i \bigvee_j l_{i,j}\) with the \(l_{i,j}\) literals.

Name: An underconstrained CNF
Definition: A CNF such that the number of clause is relatively few, compared to the number of symbols.
Page: 268
Chapter: 7
Section: 6.3

Name: An overconstrained CNF
Definition: A CNF that has many clauses relatively to the number of symbols.
Page: 268
Chapter: 7
Section: 6.3

Definition: A random \(k\)-CNF sentence with \(m\) clauses and \(n\) symbols.
Page: 268
Chapter: 7
Section: 6.3
Notation: \(CNF_k(m,n)\)

Name: \(X_i\) is arc consistent with respect to \(X_j\)
Definition: For every value in \(D_i\), there is some value in \(D_j\) that satisfies the binary constraint on the arc \((X_i,X_j)\).
Page: 212
Chapter: 6
Section: 2.2
Variables: \(P=(X,D,C)\) a (binary) CSP
\(X_i,X_j\in X\)

Name: \(X_i\) is generalized arc consistent with respect to \(C_j\)
Definition: For every value \(v\in D_i\), there exists a tuple of values that is a member of the constraint \(C_j\), has all its values taken from the domains of the corresponding variables, and has its \(X_i\) component equal to \(v\).
Page: 214
Chapter: 6
Section: 2.2
Variables: \(P=(X,D,C)\) a (binary) CSP
\(C_j\in C\),
\(X_i\in X\) appearing in \(C_j\)

Name: Satisfiability threshold conjecture
Definition: There is a threshold ratio \(r_k\) such that, as \(n\) goes to infinity, the probability that \(CNF_k(n,r_kn)\) is satisfiable becomes \(1\) for all values of \(r\) below the threshold, and 0 for all values above.
Page: 268
Chapter: 7
Section: 6.3
Variables: \(k\ge 3\)

Name: A fluent aspect of the world
Definition: An aspect of the world that changes.
Page: 270
Chapter: 7
Section: 7.1

Name: Atemporal variables
Definition: A symbol associated with permanent aspect of the world.
Page: 270
Chapter: 7
Section: 7.1

Name: Effect axiom
Definition: An axiom which describe how the world changes.
Page: 271
Chapter: 7
Section: 7.1

Name: Frame axiom
Definition: The axiom which states what does not change from one time stamp to the next one.
Page: 271
Chapter: 7
Section: 7.1

Name: Representationnal frame problem
Definition: The problem of having only \(O(k)\) frame axioms for this fluent.
Page: 271
Chapter: 7
Section: 7.1
Variables: \(k\in\mathbb N\)
\(F\) a fluent changing \(k\) times

Name: Qualification problem
Definition: The problem of stating all condition for an action to have an effect.
Page: 273
Chapter: 7
Section: 7.1

Name: A hybrid agent
Definition: a KB to represents states of the world, and
Page: 273
Chapter: 7
Section: 7.2
Context: Knowledge AI
Definition2: search algorithm to decide its actions.
Conjdef: An agent using

Name: Conservative approximation
Definition: An approximation of the state of the world, which does not forbid anything which is in fact possible.
Page: 275
Chapter: 7
Section: 7.3
Example: Representation of the world using 1-CNF formulas
Name2: Outer envelope

Name: Precondition axiom
Definition: The axiom stating that an action implies its precondition.
Page: 278
Chapter: 7
Section: 7.4
Example: Shooting at time \(t\) implies HaveArrow at time \(t\)

Page: 277
Implementation: For \(t\) from 0 to some maximal time, transform «there exists a solution in time \(t\)» to CNF. Try to solve it. If there is a model, extract a solution and return it. Otherwise, return failure.
Section: 7.4
Chapter: 7
Name: SATPlan

Name: Action exclusion axiom
Definition: An axiom stating that no 2 actions can happens at the same time.
Page: 278
Chapter: 7
Section: 7.4

Q: Natural's language is used for [...] and not for [...].
A: communication; representation of information
Page: 291
Chapter: 8
Section: 1.1

Name: Ambiguity
Definition: The fact that se same thing may have multiple meanings.
Page: 292
Chapter: 8
Section: 1.1
Variables: In natural language

Name: Ontological commitment
Definition: What a logic assumes about the nature of reality.
Page: 294
Chapter: 8
Section: 1.2

Name: Epistemological commitment
Definition: The characterization of a logic, by the possible states of knowledge allowed by a logic with respect to each fact.
Page: 294
Chapter: 8
Section: 1.2

Name: Domain of \(M\)
Definition: Set of object contained by \(M\).
Page: 294
Chapter: 8
Section: 2.1
Variables: \(M\) a model
Name2: Domain element of \(M\)

Name: A relation over \(M\)
Definition: A set of tuples of objects.
Page: 296
Chapter: 8
Section: 2.1
Variables: \(M\) a model

Name: Basic symbols in first-order logic
Definition: constant
Page: 297
Chapter: 8
Section: 2.2
Definition2: predicate,
Conjdef: All of
Definition3: function.

Name: The arity of a symbol
Definition: The number of arguments of a symbol.
Page: 297
Chapter: 8
Section: 2.2

Name: The interpretation of \(S\) in \(M\)
Definition: A specification from symbols to constant, relations and functions.
Page: 297
Chapter: 8
Section: 2.2
Variables: \(S\) a set of symbols
\(M\) a model

Name: A term
Definition: A constant or a function applied to a tuple of terms.
Page: 299
Chapter: 8
Section: 2.3
Variables: In FO

Name: Atomic sentence in First-Order Logic
Definition: A predicate, applied to a tuple of terms.
Page: 300
Chapter: 8
Section: 2.3

Name: \(A\) is true in \(M\)
Definition: The relation referred to by \(A\) holds among the objects referred to by the arguments.
Page: 300
Chapter: 8
Section: 2.4
Variables: \(S\) a set of terms,
\(A\) an atomic sentence,
\(M\) a model

Name: for all
Page: 300
Chapter: 8
Section: 2.6
Context: First-Order Logic
Notation: \(\forall\)

Name: A ground term in First-Order Logic
Definition: A term without variables
Page: 300
Chapter: 8
Section: 2.6

Definition: For all \(x\), \(P\).
Page: 301
Chapter: 8
Section: 2.6
Variables: \(P\) a logical expression
Notation: \(\forall x\, P\)

Name: \(\forall x\, P\) is true
Definition: For all extended interpretation of \(M\), \(P\) holds.
Page: 301
Chapter: 8
Section: 2.6
Variables: \(P\) a logical expression,
\(x\) a variable,
\(M\) a model

Name: There exists \(x\) such that
Page: 302
Chapter: 8
Section: 2.6
Notation: \(\exists x\)

Name: \(\exists x\, P\) is true in \(M\)
Definition: There exists an extension of \(M\) in which \(P\) is true.
Page: 302
Chapter: 8
Section: 2.6
Variables: \(P\) a formula,
\(M\) a model.

Smaller0: \(\exists x\,\neg P\)
Greater0: \(\neg\forall x\, P\)
Page: 302
Chapter: 8
Section: 2.6
Smaller to greater: is equivalent to

Name: Unique name assumption
Definition: Every constant symbol refer to a distinct object.
Page: 304
Chapter: 8
Section: 2.8

Name: Closed-world assumption
Definition: Every atomic sentences, not known to be true, are in fact false.
Page: 304
Chapter: 8
Section: 2.8

Name: Domain closure
Definition: Each model contains no more domain elements than those named by the constant symbols.
Page: 304
Chapter: 8
Section: 2.8

Name: A substitution
Definition: A value for each variables, such that the interpretation of the formula is true in \(M\).
Page: 306
Chapter: 8
Section: 3.1
Variables: \(x_1,\dots,x_n\) variables,
\(M\) a model,
\(P\) a formula
Name2: Binding list

Name: An axiom which defines \(P\)
Definition: An axiom of the form \(\forall x_1,\dots,x_n\, P(x_1,\dots,x_n)\iff F(x_1,\dots,x_n)\) with \(F\) a formula.
Page: 307
Chapter: 8
Section: 3.2
Variables: \(P(x_1,\dots,x_n)\) a predicate

Name: A theorem
Definition: A formula entailed by the axioms.
Page: 307
Chapter: 8
Section: 3.2

Name: Infix notation
Definition: Writting the name of a binary function between its two argument.
Page: 308
Chapter: 8
Section: 3.3

Name: Prefix notation
Definition: Writting the name of a function before its arguments.
Page: 309
Chapter: 8
Section: 3.3

Name: Syntactic sugar
Definition: An extension of the syntax which does not change the semantic.
Page: 309
Chapter: 8
Section: 3.3

Name: The set of natural numbers
Definition: Contains 0, and succesors of elements of this set.
Page: 308
Chapter: 8
Section: 3.3

Name: Knowledge engineering
Definition: Knowledge-base construction.
Page: 312
Chapter: 8
Section: 4

Name: Knowledge acquisition
Definition: Exctract knowledge from expert.
Page: 312
Chapter: 8
Section: 4.1

Name: The ontology of a domain
Definition: A particular theory of the nature of being or existence
Page: 312
Chapter: 8
Section: 4.1

Name: Universal Instantiation rule
Definition: Given \(v\) a variable, \(\alpha\) a formula and \(g\) a ground terme
[latex]
\begin{prooftree}
\AxiomC{$\forall v\ \alpha$}
\UnaryInfC{\textsc{SUBST}$(\{v/g\},\alpha)$}
\end{prooftree}
[/latex]
Page: 328
Chapter: 9
Section: 1
Abbreviation: UI rule

Name: Existential Instantiation rule
Definition: Given \(v\) a variable, \(\alpha\) a formula and \(k\) a constant symbol not appearing anywhere
[latex]
\begin{prooftree}
\AxiomC{$\exists v\ \alpha$}
\UnaryInfC{\textsc{SUBST}$(\{v/k\},\alpha)$}
\end{prooftree}
[/latex]
Page: 328
Chapter: 9
Section: 1

Name: A Skolem constant
Definition: The symbol introduced in the proof by the existential quantification.
Page: 328
Chapter: 9
Section: 1

Name: Inferential equivalent set of sentences
Definition: Sentences which are all equivalently satisfiable.
Page: 328
Chapter: 9
Section: 1

Name: Proposionalization
Definition: Reducing first-order logic problem to propositional problems.
Page: 329
Chapter: 9
Section: 1.2

Smaller0: \(K\) entails \(S\)
Greater0: a finite subset of \(K\) entails \(S\)
Page: 329
Chapter: 9
Section: 1.2
Variables: \(S\) a sentence,
\(K\) a first-order KB
Smaller to greater: iff

Name: Generalized Modus Ponens
Definition: Let \(p_1,p'_1\dots,p_n,p'_n,q\) propositions, \(\theta\) a substitution such that \(\text{Subst}(\theta,p_i')=\text{Subst}(\theta,p_i)\), then
[latex]
\begin{prooftree}
\AxiomC{$p_1',\dots,p_n'$}
\AxiomC{$(p_1\land \dots\land p_n\implies q)$}
\BinaryInfC{\textsc{SUBST}$(\theta,q)$}
\end{prooftree}
[/latex]
Page: 330, 331
Chapter: 9
Section: 2

Name: Lifted rule
Definition: An adaptation of \(P\) to first-order logic.
Page: 331
Chapter: 9
Section: 2
Variables: \(R\) a rule relating to propositional logic

Name: A unifier of \(p\) and \(q\)
Definition: A substitution \(\theta\) such that [$]\textsc{Subst}(\theta,p)=\textsc{Subst}(\theta,q)[/$].
Page: 331
Chapter: 9
Section: 2.2
Variables: \(p,q\) two sentences

Name: Unification
Definition: The process of finding unifiers.
Page: 331
Chapter: 9
Section: 2.2

Name: Standardizing appart
Definition: Given a set of sentences, change the name of its free-variables to obtain distinct variables in each sentences.
Page: 332
Chapter: 9
Section: 2.2

Name: \(\theta\) is more general than \(\theta'\)
Definition: \(\theta\)'s substitutions appear in \(\theta'\).
Page: 332
Chapter: 9
Section: 2.2
Variables: \(\theta,\theta'\) two substitutions

Name: Most general unifier
Definition: An unifier \(\theta\) of \(p\) and \(q\) such that, for all unifiers \(\theta'\), \(\theta\) is more general than \(\theta'\).
Page: 332, 333
Chapter: 9
Section: 2.2, 2.3
Variables: \(p,q\) sentences
Definition2: Their highest common descendant
Abbreviation: mgu

Name: Occur check
Definition: Testing whether a variable occur in a complex term.
Page: 332
Chapter: 9
Section: 2.2

Page: 332
Implementation: If \(\theta\) is failure, return failure
elsif \(x=y\) return \(\theta\)
elsif \(x\) is a variable return [$]\textsc{Unify-Var}(x,y,\theta)[/$]
elsif \(y\) is a variable return [$]\textsc{Unify-Var}(y,x,\theta)[/$]
elsif \(x\) and \(y\) are compound terms, obtained by the same operator, then return Fold Unify (the set of arguments) \(\theta\).
Section: 2.3
Chapter: 9
Effect: the most general unifier of \(x\) and \(y\) containing \(\theta\)
Variables: \(x,y\) two terms
\(\theta\) a substitutition

Name: Predicate indexing
Definition: Storing every fact related to distinct predicates in distinct buckets.
Page: 328
Chapter: 9
Section: 2.3
Context: KB

Name: The subsumption lattice
Definition: The set of terms, with the order relation «is more specific than».
Page: 329
Chapter: 9
Section: 2.3

Name: A fixed point of the inference process
Definition: A superset \(T\) of \(S\) such that no new facts can be derived from \(T\).
Page: 335
Chapter: 9
Section: 3.2
Variables: \(S\) be a set of implication sentences and fact in first order logic

Page: 332
Section: 3.2
Chapter: 9
Variables: A KB and
\(\alpha\) a query
Name: FOL-FC-ASK
Returns: A substitution for the query

Name: Pattern matching
Definition: Given a KB and a term, finding an unifier of the term and of some element of the KB.
Page: 333
Chapter: 9
Section: 3.3

Name: Conjunct ordering problem
Definition: Given a conjunction of fact and a KB, choosing the order in which to consider the conjuncts to minimize time spent to try to pattern match them to the content of the KB.
Page: 333
Chapter: 9
Section: 3.3

If a knowledge base is a haystack, and a sentence \(\alpha\) is a needle, then entailment is like the needle being in the stack and inference is like finding the needle.
Page: 242
Chapter: 7
Section: 4

Page: 261
Implementation: for each clause \(\neg x_1\lor\dots\lor\neg x_n\land y\), and \(x_1,\dots,x_n\) in \(KB\), add \(y\) to \(KB\). If the goal is found, return true. If no new fact can be derived, return false
Section: 5.4
Chapter: 7
Variables: \(KB\) a set of propositional definitie clauses
Name: Forward chaining algorithm
Time complexity: linear

Page: 266
Implementation: Input: a set of clause and a partial interpretation
Testing whether every clause is true or some clause is false. In this case answer.
Otherwise, check for pure symbol, and set them to true.
While there are unit clauses, set their litterals to true.
Choose some symbol \(P\), call itself recursively to the formula with \(P\) equal true or equal false
Section: 6
Chapter: 7
Name: DPLL
Etymology: Initial of the authors

Name: WalkSAT
Definition: Given a CNF formula, and an assignation of its variable:
-randomly, either:
--choose a random variable and flip it.
--choose a variable of an unsatifiable clause and flip it.
Page: 266
Chapter: 7
Section: 6.2

Name: A children of \(n\)
Definition: \(n\) plus a single substitution.
Page: 333
Chapter: 9
Section: 2.3
Variables: \(L\) a subsumption lattice,
\(n\) a node

Instruction: Tell
Page: 239
Effect: Send information to a knowledge agent
Chapter: 7
Extra: prog

Instruction: Ask
Page: 239
Effect: Query information from a knowledge agent
Chapter: 7
Extra: prog

Instruction: AskVars(
  KB,
  P(x,...,z)
)
Page: prog
306
Effect: Ask for variables such that \(P(x,...,z)\) is true.
Language: pseudocode
Chapter: 8
Section: 3.1
Extra: prog

Name: Successor-state axiom
Definition: Axiom stating that \(F\) at time \(t+1\) is true if either:
-it is true at time \(t\) and it did not became false
-it becomes true.
Page: 272
Chapter: 7
Section: 7.1
Variables: \(F\) a Boolean fluent
\(t \) a time

Question: Heuristic to avoid generating many time the same fact in forward chaining ?
Answer: A generation of \(B\) using a rule \(\bigwedge A_i\implies B\) is done only if some \(A_i\) has been introduced in the last run of the main loop
Page: 334
Chapter: 9
Section: 3

Name: Rete algorithm
Definition: An algorithm, which transform a CSP into a dataflow. A graph whose variables flow through edges, and nodes correspond to hypothesis
Page: 335
Chapter: 9
Section: 3
Variables: \(P\) a CSP

Name: Production system
Definition: Earliest forward-chaining systems in widespread use
Page: 336
Chapter: 9
Section: 3
Variables: \(P\) a CSP

Name: Cognitive architectures
Definition: Model of human reasoning
Page: 336
Chapter: 9
Section: 3

Name: Source of inefficiency in forward chaining
Page: 335, 336
Chapter: 9
Section: 3
Example: Generating many time the same fact
Example2: Irrelevant facts

Name: Deductive database
Page: 335, 336
Chapter: 9
Section: 3
Intuition: like relational databases, but which use forward chaining as the standard inference tool rather than SQL queries

Name: Magic set
Definition: A set of selected variable bindings, chosen according to the goal. Those are the only bindings considered in a forward checking algorithm.
Page: 336
Chapter: 9
Section: 3

Name: A generator
Definition: A function returning multiple time
Page: 337
Chapter: 9
Section: 4

Smaller0: Algorithm
Greater0: Logic
Page: 339
Chapter: 9
Section: 4.2
Smaller to greater: =
Hide middle: yes
Name: Robert Kowalski’s equation
Greater1: Control
Connect Greater0: +

Name: Prolog
Definition: Most widely used logic programming language
Page: 339
Chapter: 9
Section: 4.2
Definition2: Sets of definite clauses

Instruction: Word with first letter capitalized
Page: 339
Effect: Variable
Context: Prolog
Chapter: 9
Section: 4.2

Instruction: Word with first letter not capitalized
Page: 339
Effect: Constant and predicate
Context: Prolog
Chapter: 9
Section: 4.2

Instruction: foo :- bar_1, ..., bar_n
Page: 339
Effect: If each bar_i holds for some variable bindings, then foo also holds for the same variables
Context: Prolog
Chapter: 9
Section: 4.2

Instruction: []
Page: 339
Effect: Empty list
Context: Prolog
Chapter: 9
Section: 4.2

Instruction: [A_1,...,A_n |B]
Page: 339
Effect: list with head A_1,...,A_n and tail B
Context: Prolog
Chapter: 9
Section: 4.2

Name: A choice point
Definition: A point in the execution where prolog have choosen one choice out of many
Page: 340
Chapter: 9
Section: 4.3
Context: Prolog

Name: Warren abstract manchine
Definition: One of the implementers of the first Prolog compiler.
Page: 340
Chapter: 9
Section: 4.3
Abbreviation2: WAM

Name: Continuation
Definition: Packaging up a procedure and a list of arguments that together define what should be done next whenever the current goal succeeds
Page: 341
Chapter: 9
Section: 4.3

Name: Or-parallelism
Definition: a goal unifying with many different clauses in the knowledge base. Each gives rise to an independent branch in the search space that can lead to a potential solution, and all such branches can be solved in parallel.
Page: 342
Chapter: 9
Section: 4.3
Context: Prolog

Name: AND-parallelism
Definition: Solving each conjunct in the body of an implication in parallel
Page: 342
Chapter: 9
Section: 4.3
Context: Prolog

Question: Problem with the program
path(X,Z) :- path(X,Y), link(Y,Z).
path(X,Z) :- link(X,Z).
Page: 342
Chapter: 9
Section: 4.4
Context: Prolog

Name: Memoization
Definition: caching solutions to subgoals as they are found and then reusing those solutions when the subgoal recurs, rather than repeating the previous computation.
Page: 343
Chapter: 9
Section: 4.4

Name: tabled logic programming
Definition: A system using efficient storage and retrieval mechanisms to perform memoization
Page: 343
Chapter: 9
Section: 4.4
Context: Inference in First-Order Logic

Name: The completion of \(E\)
Definition: A First-order formula stating that the assertion of \(E\) are the only one satisfying the predicate used in \(E\)
Page: 344
Chapter: 9
Section: 4.5
Variables: \(E\) a list of assertion

Name: Constraint Logic Programming
Definition: Programming by constraining variables
Page: 345
Chapter: 9
Section: 4.6
Abbreviation: CLP

Question: Constraint Logic Programming restricted to equality is
Answer: CSP
Page: 345
Chapter: 9
Section: 4.6