CSC 411 1st Edition Lecture 20 Outline of Last Lecture I. Knowledge-based agentsII. Wumpus worldIII. LogicOutline of Current Lecture I. Logic & propositional logicII. Inference rules and theorem provinga. Truth table approachb. Inference rules approachc. Satisfiability and Resolution RefutationCurrent Lecture Knowledge Representationo Objective: express the knowledge about the world in a computer-tractable formo Knowledge representation languages (KRLs)o Inference procedures: a set of procedures that us the KRLs to infer new facts from known ones or answer a variety of KB queries Typically require a search Logical Inference Problemo Given: A knowledge base KB (a set of sentences)  A sentence  (called a theorem)o Does KB semantically entail ? KB |= ?o In other words: In all interpretations in which the sentences in KB are true,  is also true Sound and Complete Inferenceo Inference is a process by which conclusions are reached We want to implement the inference process on a computero Assume an inference procedure i that derives a sentence  from the KB:  KB |—i o Properties of the inference procedure in terms of entailment Soundness: An inference is sound if KB |—i , then we have KB |=  Completeness: if KB|= , then KB |—i These notes represent a detailed interpretation of the professor’s lecture. GradeBuddy is best used as a supplement to your own notes, not as a substitute. Solving Logical Inference Problemo How to design the procedure that answers KB|= ?o Three approaches Truth-table approach Inference rules Conversion to the inverse SAT problem – Resolution refutation Truth-Table Approacho Two-step procedure Generate table for all possible interpretations Check whether the sentence  evaluates to true whenever KB evaluates to trueo Sound and complete Limitations of Truth-Tableo What is the computational complexity? Exponential in the number of the propositional symbols:- 2n rows in the tableo How to make the process more efficient? Observation: KB is only true on a small subset of interpretationso Solution: inference rules approach Start from entries for which KB is true Generate new (sound) sentences from the existing ones Inference Rules Approacho Start from KBo Infer new sentences that are true from existing KB sentenceso Repeat until  is proved (inferred true) or no more sentences can be provedo Rules: Let us generate new (sound) sentences from existing oneso Equivalence rules Known logical equivalenceso Inference Rules Represent sound “local” inference patterns Logical equivalenceo The propositions P and Q are called logically equivalent if PQ is a tautology (same truth table). The notation PQ denotes P and Q are logically equivalent Important Logical Equivalencieso Identity pT  p pF  po Domination pT  T pF  Fo Idempotent pp  p pp  po Double negation (p)  po Commutative pq  qp pq  qpo Associative (p  q)  r  p  (q  r) (p  q)  r  p  (q  r)o Distributive p  (q  r)  (p  q)  (p  r) p  (q  r)  (p  q)  (p  r)o DeMorgan (p  q)  p  q (p  q)  p  qo Other useful equivalencies p  p  T p  p  F pq  p  q Inference Ruleso Modus Ponens Premise: AB, A Conclusion: B If both sentences in the premise are true then the conclusion is true Soundo And-elimination Premise: A1A2A3 An Conclusion: Aio And-introduction Premise: A1, A2, A3, …. An Conclusion: A1A2A3 Ano Or-introduction Premise: Ai Conclusion: A1A2A3 Ano Unit resolution Premise: AB, A Conclusion: Bo Resolution Premise: AB, AC Conclusion: BCo All of the above inference rules are sound. We can prove this through truth tables Logical Inferences and Searcho To show that theorem  holds for a KB, we may need to apply a number of soundinference rules Problem: many possible rules can be applied Instance of a search problem:- Truth table method (from the search perspective): blind enumeration and checkingo Inference rule method as a search problem State: a set of sentences that are known to be true Initial state: a set of sentences in the KB Operators: applications of inference rules Goal state: a theorem  is derived from KBo Logical inference Proof: a sequence of sentences that are immediate consequences of applied inference rules Theorem proving: process of finding a proof of a theorem Normal Formso Problems: Too many different rules one can apply Many new sentences are just equivalent sentenceso Question: Can we simplify inferences using one of the normal forms?o Normal forms Conjunctive normal form (CNF): conjunction of clauses (clauses include disjunctions of literals- (AB)  (CDJ)  (E G) Disjunctive normal form (DNF): disjunction of terms (terms include conjunction of literals- (AB)  (AC)  (CD)o Conversion to a CNF Key fact: it is always possible to convert any KB to a CNF Assume: (AB)  (CA) Eliminate , - (AB)  (CA) Reduce the scope of signs through DeMorgan Laws and double negation- (AB)  (CA) Convert to CNF using associative and distributive laws- (A  C  A)  (B  C  A)- (A  C)  (B  C  A) Resolution Ruleo Sound inference that fits the CNFo If a literal appears in one clause and its negation appears in the other one, the two clauses can be merged and that literal can be discardedo Not complete – repeated application of the resolution rule to a KB in CNF may failto derive new valid sentenceso Example:  We know: (AB) We want to show: (AB) Resolution rule fails to derive it Satisfiability (SAT) Problemo Determine whether a sentence in the CNF is satisfiable (i.e. can evaluate to true)o Instance of a constraint satisfaction problem: Variables:- Propositional symbols- Values (True, False) Constraints:- Every conjunct must evaluate to true, at least one of the literals in each clause must evaluate to true Inference problem and satisfiabilityo Inference problem: We want to show that  is a sentence