knowledge base

a set of sentences. - inference:deriving new sentences from old - TELL: add new sentences to the knowledge base - ASK: a way to query what is known. The standard names for these operations

Generic KB-Based Agent

Similar to agents with internal states.

1
2
3
4
5
6
7
8

function KB-Agent(percept) returns an action
  static KB = a knowledge base, 
         t = 0 // a counter indicating time
  tell(KB, make_percept_sentence(percept, t))
  action = ask(KB, make_action_query(t))
  tell(KB, make_action_sentence(action, t))
  t++
  return action

Agent must be able to: - Represent stats and actions; - Incorporate new percepts; - Update internal representation of the world; - Deduce hidden properties of the world; - Deduce appropriate actions.

logic

• Syntax: what expressions are legal
  

• Semantics: what legal expression mean

• entailment: α $\models$ β if and only if, in every model in which α is true, β is also true.
• Models: M(alpha) = set of all models of alpha: alpha $\models$ beta if and only if M(alpha) $\subseteq$ M(beta)
  
• Soundness: An inference algorithm that derives only entailed sentences is called sound or truth- preserving.

• Completeness: an inference algorithm is complete if it can derive any sentence that is entailed.

Propositional logic:

• Syntax: $\neg \wedge \vee \Rightarrow ()implication \Leftrightarrow (biconditional)$
• sematic:
• ¬P is true iff P is false in m.
• P ∧ Q is true iff both P and Q are true in m.
• P ∨ Q is true iff either P or Q is true in m.
• P ⇒ Q is true unless P is true and Q is false in m.
• P ⇔ Q is true iff P and Q are both true or both false in m.

Truth tables (model checking)

• True table enumeration algorithm is sound and complete
• Time: $O(2^n)$, n symbols
• Space: $O(n)$

Standard logical equivalences: α≡β if and only if α |= β and β |= α - (α ∧ β) ≡ (β ∧ α) commutativity of ∧ - (α ∨ β) ≡ (β ∨ α) commutativity of ∨ - ((α ∧ β) ∧ γ) ≡ (α ∧ (β ∧ γ)) associativity of ∧ - ((α ∨ β) ∨ γ) ≡ (α ∨ (β ∨ γ)) associativity of ∨ - ¬(¬α) ≡ α double-negation elimination - (α ⇒ β) ≡ (¬β ⇒ ¬α) contraposition - (α ⇒ β) ≡ (¬α ∨ β) implication elimination - (α ⇔ β) ≡ ((α ⇒ β) ∧ (β ⇒ α)) biconditional elimination - ¬(α ∧ β) ≡ (¬α ∨ ¬β) De Morgan - ¬(α ∨ β) ≡ (¬α ∧ ¬β) De Morgan - (α ∧ (β ∨ γ)) ≡ ((α ∧ β) ∨ (α ∧ γ)) distributivity of ∧ over ∨ - (α ∨ (β ∧ γ)) ≡ ((α ∨ β) ∧ (α ∨ γ)) distributivity of ∨ over ∧

Theorem proving

• A sentence is valid if it is true in all models
• Deduction theorem: for any sentences α and β, α $\models$ β if and only if the sentence (α ⇒ β) is valid.
• A sentence is satisfiable if it is true in, or satisfied by, some model. α |= β if and only if the sentence (α ∧ ¬β) is unsatisfiable.
• Modus Ponens: whenever any sentences of the form α ⇒ β and α are given, then the sentence β can be inferred.
  $\frac{\alpha \Rightarrow \beta, \beta}{\beta}$
• And-Elimination: $\frac{\alpha \wedge \beta}{\alpha}$
• monotonicity: the set of entailed sentences can only increase as information is added to the knowledge base. $ if KB then KB $

• unit clause, where clause is a disjunction of literals: $\frac{l_1 \vee ... \vee l_k , m_1 \vee ... \vee m_n}{l_1 \vee ... \vee l_{i-1} \vee l_{i+1} \vee m_1 \vee \vee m_{j-1} \vee m_{j+1} \vee ... \vee m_n}$

• conjunctive normal form:A sentence expressed as a conjunction of clauses

• Resolution Algorithm:

  1 2 3 4 5 6 7 8 9 10

  function PL-Resolution(KB, a) returns true or false clauses = the set of clauses in the CNF representation of KB and not a new = {} loop do for each Ci, Cj in clauses do resolvents = PL-Resolution(Ci, Cj) If resolvents contains the empty clause return true new = new U resolvents if new belongs to clauses then return false clauses = clauses U new

Horn clauses

Forward chaining

• ← Previous Post
• Next Post →