Knowledge-based agents
Knowledge base = set of sentences in a formal language
Basic actions:Ask/Tell
- A knowledge base keeps track of things
- we can TELL it facts and ASK for inference
At every step:
- Construct a sentence with assertion about percepts
- Construct a sentence asking what action is next
- Construct a sentence asserting that action
Logic in general
Basic concepts
Logics are formal languages for representing information such that conclusions can be drawn
Syntax defines the sentences in the language
Semantics define the “meaning” of sentences, i.e., define truth of a sentence in a world
Entailment
Entailment means that one thing follows from another: $KB$ |= $\alpha$
Knowledge base KB entails sentence α if and only if where KB is true, α is also true
Entailment is a relationship between sentences (i.e., syntax) that is based on semantics
Models
Logicians typically think in terms of models, which are formally structured worlds with respect to which truth can be evaluated, which means models describe possible worlds.
We say m is a model of a sentence α if α is true in m
$M(α)$ is the set of all models of $α$
$KB$ |= $α$, if and only if $M(KB) \subseteq M(α)$
Logical equivalence
Two sentences are logically equivalent iff true in same models:
$α ≡ β$ if and only if $α$ |= $β$ and $β$ |= $α$
Validity and satisfiability
Validity: it is true in all models
Deduction: $α$ |= $β$ iff $α \Rightarrow β$
Satisfiability: if some model makes it true
Unsatisfiable: if it is true in no models
Inference: Forward chaining & Backward chaining
Horn Form
- KB conjunction of Horn clauses
- Horn Clause(at most one literal is Positive)
- For examples: $（¬ P \bigvee ¬Q\bigvee V)$ is a Horn Clause
- so is $(¬ P \bigvee ¬ Q)$, but $(¬P \bigvee Q\bigvee V)$ is not
- Definite Clauses: exactly one literal is positive
- Horn Clauses can be re-written as implications:
- proposition symbol(fact) or
- conjunction of symbols (body or premise) $\Rightarrow$ symbol(head)
- Examples: $(¬ C \bigvee ¬ B \bigvee A)$ becomes $(C\bigwedge B \Rightarrow A)$, because $(\alpha \Rightarrow \beta \equiv (¬ \alpha \bigvee \beta))$
Video about the process of FC and BC
Resolution
CNF
conjunction of disjunctions of literals(clauses)
E.g., $(A ∨ ¬B) ∧ (B ∨ ¬C ∨ ¬D)$
More details about CNF in wiki
Resolution Algorithm
Proof by contradiction, i.e., show $KB ∧ ¬α$ unsatisfiable to prove $KB$ |= $α$ satisfiable