Propositional logic: Horn clauses

1 1CS 2740 Knowledge RepresentationM. HauskrechtCS 2740 Knowledge RepresentationLecture 6 Milos Sennott SquarePropositional logic: horn clauses CS 2740 Knowledge RepresentationM. HauskrechtAdministration Homework assignment 2 Propositional logic exercises Programming a resolution solver2CS 2740 Knowledge RepresentationM. HauskrechtLogical inference problemLogical inference problem: Given: a knowledge base KB (a set of sentences) and a sentence (called a theorem), Does a KB semantically entail?In other words: In all interpretations in which sentences in the KB are true, is also true? =|KB? CS 2740 Knowledge RepresentationM. HauskrechtSolving logical inference problemIn the following:How to design the procedure that answers: Three approaches: Truth-table approach Inference rules Conversion to the inverse SAT problem Resolution-refutation =|KB?3CS 2740 Knowledge RepresentationM. HauskrechtKB in restricted formsIf the sentences in the KB are restricted to some special forms some of the sound inference rules may become completeExample: horn form ( horn normal form) Two inference rules that are sound and complete with respect to Propositional symbolsfor KBs in the horn normal form: Resolution (positive unit resolution) Modus ponens)()(DCABA ))(()(DCAAB Can be written also as:CS 2740 Knowledge RepresentationM.

2 HauskrechtKB in horn form horn form:a clause with at most one positive literal Not all sentences in Propositional logic can be converted into the horn form KB in horn normal form: Three types of Propositional statements: Rules Facts Integrity constraints)()(DCABA )(21 ABBBk KB)(21 ABBBk K))((21 ABBBk K)(21kBBB K)(21 FalseBBBk K4CS 2740 Knowledge RepresentationM. HauskrechtKB in horn form horn form:a clause with at most one positive literal Not all sentences in Propositional logic can be converted into the horn form KB in horn normal form: Three types of Propositional statements: Rules Facts Integrity constraints)()(DCABA )(21 ABBBk KB)(21 ABBBk K))((21 ABBBk K)(21kBBB K)(21 FalseBBBk KCS 2740 Knowledge RepresentationM. HauskrechtKB in horn form Modus ponens: More general version of the rule: Modus ponens is sound and complete with respect to Propositional symbolsfor the KBs in the horn normal form We assume only logical inference problems for which the theorem is a Propositional symbol: Note:no negation of a Propositional symbol is allowedABAB, ABBBABBBkkKK,,,)(2121 5CS 2740 Knowledge RepresentationM.

3 HauskrechtKB in horn form Inferences: Resolution rule: Resolution is sound and complete with respect to Propositional symbolsfor the KBs in the horn normal form CACBBA ,CS 2740 Knowledge RepresentationM. HauskrechtComplexity of inferences for KBs in HNFQ uestion:How efficient the inferences in the HNF wrt Propositional symbols can be? Answer:Procedures linear in the size of the KB in the horn form exist. Size of a clause: the number of literals it contains. Size of the KB in the HNF: the sum of the sizes of its : )(),(),(),(,,GFEECDCCBABA )(),(),(),(,,GFEECDCCBABA The size is: 12or6CS 2740 Knowledge RepresentationM. HauskrechtComplexity of inferences for KBs in HNFHow to do the inference? If the HNF (is in clausal form) we canapply resolution. )(),(),(),(,,GFEECDCCBABA CB CDECS 2740 Knowledge RepresentationM. HauskrechtComplexity of inferences for KBs in HNFF eatures: Every resolution is a positive unit resolution; that is, a resolution in which one clause is a positive unit clause( , a proposition symbol).

4 (),(),(),(,,GFEECDCCBABA CB CDE7CS 2740 Knowledge RepresentationM. HauskrechtComplexity of inferences for KBs in HNFF eatures: At each resolution, the input clause which is not a unit clause is a logical consequence of the result of the resolution. (Thus,the input clause may be deleted upon completion of the resolution operation.))(),(),(),(,,GFEECDCCBABA CB CDECS 2740 Knowledge RepresentationM. HauskrechtComplexity of inferences for KBs in HNFF eatures: At each resolution, the input clause which is not a unit clause is a logical consequence of the result of the resolution. (Thus,the input clause may be deleted upon completion of the resolution operation.))(),(),(),(,,GFEECDCCBABA CB CDE8CS 2740 Knowledge RepresentationM. HauskrechtComplexity of inferences for KBs in HNFF eatures: Following this deletion, the size of the KB (the sum of the lengths of the remaining clauses ) is one less than it was beforethe operation.)

5 (),(),(),(,,GFEECDCCBABA CB CDECS 2740 Knowledge RepresentationM. HauskrechtComplexity of inferences for KBs in HNFF eatures: If n is the size of the KB, then at most n positive unit resolutions may be performed on it.)(),(),(),(,,GFEECDCCBABA CB CDE9CS 2740 Knowledge RepresentationM. HauskrechtComplexity of inferences for KBs in HNFA linear time resolution algorithm: The number of positive unit resolutions is limited to the size of the formula (n) But to assure overall linear time we need to access each proposition in a constant time: Data structures indexed by proposition names may be accessed in constant time. (This is possible if the proposition names arenumber in a range ( , ), so that array lookup is the access operation. If propositions are accessed by name, then a symbol table is necessary, and the algorithm will run in time O(n log(n)).CS 2740 Knowledge RepresentationM. HauskrechtForward and backward chainingTwo inference procedures based on modus ponensfor horn KBs: Forward chainingIdea:Whenever the premises of a rule are satisfied, infer the conclusion.))

6 Continue with rules that became satisfied. Backward chaining (goal reduction)Idea:To prove the fact that appears in the conclusion of a rule prove the premises of the rule. Continue procedures are complete for KBs in the horn form!!!10CS 2740 Knowledge RepresentationM. HauskrechtForward chaining example Forward chainingIdea:Whenever the premises of a rule are satisfied, infer the conclusion. Continue with rules that became KB:R1:R2:R3:Assume the KB with the following rules and facts:CBA EDC F1:F2:F3:ABDET heorem:? CS 2740 Knowledge RepresentationM. HauskrechtForward chaining exampleKB:R1:R2:R3:GFC CBA EDC Theorem:F1:F2:F3:ABDE11CS 2740 Knowledge RepresentationM. HauskrechtForward chaining exampleKB:R1:R2:R3:GFC CBA EDC Theorem:F4:CF1:F2:F3:ABDRule R1 is 2740 Knowledge RepresentationM. HauskrechtForward chaining exampleKB:R1:R2:R3:GFC CBA EDC Theorem:F4:CF1:F2:F3:ABDRule R1 is R2 is :EE12CS 2740 Knowledge RepresentationM. HauskrechtForward chaining Efficient implementation: linear in the size of the KB Example:BALBALPAMLBPMLQP CS 2740 Knowledge RepresentationM.

7 HauskrechtForward chaining Runs in time linear in the number of literals in the horn formulae13CS 2740 Knowledge RepresentationM. HauskrechtForward chaining** BALBALPAMLBPMLQP Agenda (facts)CS 2740 Knowledge RepresentationM. HauskrechtForward chaining BALBALPAMLBPMLQP inferred14CS 2740 Knowledge RepresentationM. HauskrechtForward chaining BALBALPAMLBPMLQP inferredadd to agendaCS 2740 Knowledge RepresentationM. HauskrechtForward chaining BALBALPAMLBPMLQP 15CS 2740 Knowledge RepresentationM. HauskrechtForward chaining BALBALPAMLBPMLQP CS 2740 Knowledge RepresentationM. HauskrechtForward chaining BALBALPAMLBPMLQP 16CS 2740 Knowledge RepresentationM. HauskrechtForward chaining BALBALPAMLBPMLQP CS 2740 Knowledge RepresentationM. HauskrechtBackward chaining example Goal: prove the theorem, try to be more theorem drivenKB:R1:R2:R3:GFC CBA EDC F1:F2:F3:ABDT heorem: EProblem: 17CS 2740 Knowledge RepresentationM.

8 HauskrechtBackward chaining example Backward chaining tries to prove a theorem Procedure idea: Checks if the theorem is true If not, find the rule with the theorem in its conclusion and try to prove its premises CR2 EDKB:R1:R2:R3:GFC CBA EDC F1:F2:F3:ABD?Theorem: ECS 2740 Knowledge RepresentationM. HauskrechtBackward chaining example Backward chaining is theorem drivenCAR1BR2 EDKB:R1:R2:R3:GFC CBA EDC F1:F2:F3:ABD18CS 2740 Knowledge RepresentationM. HauskrechtBackward chaining BALBALPAMLBPMLQP CS 2740 Knowledge RepresentationM. HauskrechtBackward chaining BALBALPAMLBPMLQP 19CS 2740 Knowledge RepresentationM. HauskrechtBackward chainingBALBALPAMLBPMLQP CS 2740 Knowledge RepresentationM. HauskrechtBackward chainingBALBALPAMLBPMLQP 20CS 2740 Knowledge RepresentationM. HauskrechtBackward chainingBALBALPAMLBPMLQP CS 2740 Knowledge RepresentationM. HauskrechtBackward chainingBALBALPAMLBPMLQP 21CS 2740 Knowledge RepresentationM.

9 HauskrechtBackward chainingBALBALPAMLBPMLQP CS 2740 Knowledge RepresentationM. HauskrechtBackward chainingBALBALPAMLBPMLQP 22CS 2740 Knowledge RepresentationM. HauskrechtBackward chaining BALBALPAMLBPMLQP CS 2740 Knowledge RepresentationM. HauskrechtBackward chaining BALBALPAMLBPMLQP 23CS 2740 Knowledge RepresentationM. HauskrechtForward vs Backward chaining FC is data-driven, automatic, unconscious processing, , object recognition, routine decisions May do lots of work that is irrelevant to the goal BC is goal-driven, appropriate for problem-solving, , Where are my keys? How do I get into a PhD program? Complexity of BC can be much lessthan linear in size of KBCS 2740 Knowledge RepresentationM. HauskrechtKB agents based on Propositional logic Propositional logic allows us to build knowledge-basedagents capable of answering queries about the world by infering new facts from the known ones Example:an agent for diagnosis of a bacterial diseaseThe stain of the organism is gram-positiveThe morphology of the organism is coccusThe growth conformation of the organism is chainsThe identity of the organism is streptococcus(If)(Then)Facts:The stain of the organism is gram-positiveThe growth conformation of the organism is chainsRules: 24CS 2740 Knowledge RepresentationM.

10 HauskrechtLimitations of the HNFThe HNF works with Propositional symbols: Only non-negated Propositional symbols may occur in the premise and the conclusion of the rule Only non-negated propositions can be used as factsDilemma: how to represent the negation so that we can express sentences like: If it is not raining we will go swimmingSolution 1:make an explicit proposition for Not_RainingSolution 2:negation as the failure The negation of the Propositional symbol will become true if we fail to prove it is trueCS 2740 Knowledge RepresentationM. HauskrechtNegation as the failureThe negation of the Propositional symbol will become true if we fail to prove it is trueCaveats:not Q PIn terms of logic we have possibilities: P=True, or Q=TrueProblem is if we use the failure to prove idea: Q is never on the right hand side of the rule so how we can prove it is not trueSolution:stable models Each atom (proposition) has a rule 25CS 2740 Knowledge RepresentationM.