06. Logical Agents II Flashcards
Explain resolution inference rules & complementary literals
slide44
Conjunctive Normal Form
The resolution rule only applies to disjunction of literals, which are also called clauses.
Fortunately, every sentence of propositional logic can be reformulated as a conjunction of clauses, which is also referred to as conjunctive normal form (CNF)
Examples:
(A∨B ∨C)∧(¬A∨B ∨C) yes
A∧B ∧C ∨(¬A∧B ∨C) no
A∧B ∧C ∧(¬A∨B ∨C) yes
Conjunctive Normal Form
A sentence with literals xij of the form Vi Wj (¬)xij is in conjunctive normal form.
A Resolution Algorithm
Inference procedures based on resolution use the principle of proof by contradiction:
To show that KB |= α, we show that…
Basic procedure
1 KB ∧ ¬α is converted into CNF
2 The resolution rule is applied to the resulting clauses:
…
3 The process continues until
there are no new clauses to be added ⇒ KBdoes not|= α;
two clauses resolve to yield the empty clause ⇒
KB ∧ ¬α is unsatisfiable.
each pair that contains complementary literals is resolved to produce a new clause, which is added to the others (if not already present)
KB |= α.
Resolution Algorithm
Propositional Theorem Proving Proof by Resolution
function PL-Resolution (KB, α) returns true, or false
clauses ← the set of clauses in the CNF representation of KB ∧ ¬α
new ← {}
…write the pseudocode
loop do
for each pair of clauses Ci ,Cj in clauses do
resolvents ← PL-Resolve(Ci ,Cj )
if resolvents contains the empty clause then return true new ← new ∪ resolvents
if new ⊆ clauses then return false
clauses ← clauses ∪ new
Completeness of Resolution
It remains to show why resolution is complete for propositional logic.
Resolution closure
The resolution closure RC(S) of a set of clauses S is the set of all clauses …
RC(S) is finite, because …
Hence, PL-resolution always terminates.
Ground resolution theorem
If a set of clauses is unsatisfiable, then the resolution closure of …
derivable by repeated application of the resolution rule to S and its derivatives.
there are only finitely many distinct clauses that can be constructed out of the symbols P1, . . ., Pk .
those clauses contains the empty clause.
Horn Clauses
Some simple forms of sentences do not require proof by resolution. We introduce Horn clauses for which very efficient inference algorithms exist.
…
Which are Horn clauses?
(L1,1 ∧ Breeze) ⇒ B1,1 yes L1,1 yes (≡ true ⇒ L1,1) (L1,1 ∨ Breeze) ⇒ B1,1 no
A knowledge base consisting of Horn clauses only requires Modus Ponens as an inference method:
Horn clause
proposition symbol; or
(conjunction of symbols) ⇒ symbol
Forward vs. Backward Chaining
Forward chaining
Forward chaining is …
It is popular in e.g., object recognition and routine decisions.
Forward chaining may …
Backward chaining
Backward chaining is goal-driven and appropriate for problem-solving.
It is a good choice for problems, such as e.g., Where are my keys? How do I cook a meal?
Computational effort of …
data-driven, automatic, and unconsciously processing.
do lots of work that is irrelevant to the goal.
backward chaining can be much less than linear in time and space.
Overview of inference methods (complete vs incomplete)
slide 81
Summary Chapter 6
Intelligent agents need …
Knowledge is contained in agents in the form of …
A knowledge-based agent is composed of a knowledge base and an inference mechanism, which infers new sentences for decision making.
The set of possible models for propositional logic is finite, so …
Inference rules are …
The resolution rule yields a complete inference algorithm for knowledge bases in …. Forward and backward chaining are …
knowledge about the world in order to reach good solutions.
sentences in a knowledge representation language that are stored in a knowledge base.
entailment can be checked by enumerating models.
patterns of sound inference to find proofs.
conjunctive normal form;natural reasoning algorithms for Horn clauses.
