人工智能(Nilson版-英文课件)-Chap13-命题演算.ppt

1、The Propositional CalculusChapter 13.2OutlinelUsing Constraints on Feature ValueslThe LanguagelRules of InferencelDefinition of ProoflSemanticslSoundness and CompletenesslThe PSAT ProblemlOther Important Topics3Using Constraints on Feature ValueslDescription and SimulationDescriptionlBinary-valued f

2、eatures on what is true about the world and what is not trueleasy to communicatelIn cases where the values of some features cannot be sensed directly, their values can be inferred from the values of other featuresSimulationlIconic representationlmore direct and more efficient4Using Constraints on Fe

3、ature ValueslMotivating ExampleConsider a robot that is able to lift a block, if that block is liftable and the robots battery power source is adequateIf both are satisfied, then when the robot tries to lift a block it is holding, its arm moves.lx1 (BAT_OK)lx2 (LIFTABLE)lx3 (MOVES)constraint in the

4、language of the propositional calculusBAT_OK LIFTABLE MOVES5Using Constraints on Feature ValueslLogic involvesA language (with a syntax)Inference ruleSemantics for associating elements of the language with elements of some subject matterlTwo logical languagespropositional calculusfirst-order predica

5、te calculus (FOPC)613.2 The LanguagelElementsAtomsltwo distinguished atoms T and F and the countably infinite set of those strings of characters that begin with a capital letter, for example, P, Q, R, , P1, P2, ON_A_B, and so on.Connectivesl, , , and , called “or”, “and”, “implies”, and “not”, respe

6、ctively.Syntax of well-formed formula (wff), also called sentenceslAny atom is a wff.lIf w1 and w2 are wffs, so are w1 w2, w1 w2, w1 w2, w1.lThere are no other wffs.713.2 The LanguagelLiteralatoms and a sign in front of themlAntecedent (前项）and Consequent （后项）In w1 w2, w1 is called the antecedent of

7、the implication.w2 is called the consequent of the implication.lExtra-linguistic separators: ( , )group wffs into (sub) wffs according to the recursive definitions.813.3 Rule of InferencelWays by which additional wffs can be produced from other oneslCommonly used rulesmodus ponens(演绎推理）演绎推理）: wff w2

8、 can be inferred from the wff w1 and w1 w2 introduction: wff w1 w2 can be inferred from the two wffs w1 and w2commutativity : wff w2 w1 can be inferred from the wff w1 w2 elimination: wff w1 can be inferred from the w1 w2 introduction: wff w1 w2 can be inferred from either from the single wff w1 or

9、from the single wff w2 elimination: wff w1 can be inferred from the wff ( w1 ).913.4 Definitions of Proof（验证定义）lProofThe sequence of wffs w1, w2, , wn is called a proof of wn from a set of wffs iff each wi is either in or can be inferred from a wff earlier in the sequence by using one of the rules o

10、f inference.lTheoremIf there is a proof of wn from , wn is a theorem of the set .l wnDenote the set of inference rules by the letter R.lwn can be proved from l R wn10ExamplelGiven a set, , of wffs: P, R, P Q, P, P Q, Q, R, Q R is a proof of Q R.lThe concept of proof can be based on a partial order.1

11、113.5 Semantics（语义）lSemanticsHas to do with associating elements of a logical language with elements of a domain of discourse.MeaninglSuch associationlInterpretationAn association of atoms with propositionsDenotation（指称）lIn a given interpretation, the proposition associated with an atom1213.5 Semant

12、icslUnder a given interpretation, atoms have values True or False.lSpecial AtomT : always has value TrueF : always has value FalselAn interpretation by assigning values directly to the atoms in a language can be specified13Propositional Truth Table lGiven the values of atoms under some interpretatio

13、n, use a truth table to compute a value for any wff under that same interpretation.lLet w1 and w2 be wffs.(w1 w2) has True if both w1 and w2 have value True.(w1 w2) has True if one or both w1 or w2 have value True. w1 has value True if w1 has value False.The semantics of is defined in terms of and .

14、 Specifically, (w1 w2) is an alternative and equivalent form of ( w1 w2) .14Propositional Truth Table (2)lIf an agent describes its world using n features and these features are represented in the agents model of the world by a corresponding set of n atoms, then there are 2n different ways its world

15、 can be.lGiven values for the n atoms, the agent can use the truth table to find the values of any wffs.lSuppose the values of wffs in a set of wffs are given.Do those values induce a unique interpretation?Usually “No.”Instead, there may be many interpretations that give each wff in a set of wffs th

16、e value True .15SatisfiabilitylAn interpretation satisfies a wff if the wff is assigned the value True under that interpretation.lModelAn interpretation that satisfies a wffIn general, the more wffs that describe the world, the fewer models.lInconsistent or UnsatisfiableWhen no interpretation satisf

17、ies a wff, the wff is inconsistent or unsatisfiable.e.g. F or P P16Validity(永真性）永真性）lA wff is said to be validIt has value True under all interpretations of its constituent atoms.e.g.lP PlTl ( P P )lQ Tl(P Q) P PlP (Q P)Use of the truth table to determine the validity of a wff takes time exponential

18、 in the number of atoms17EquivalencelTwo wffs are said to be equivalent iff their truth values are identical under all interpretations.lDeMorgans laws(w1 w2) w1 w2(w1 w2) w1 w2lLaw of the contrapositive(w1 w2) (w2 w1)lIf w1 and w2 are equivalent, then the following formula is valid:(w1 w2) (w2 w1)18

19、Entailment（涵蕴）涵蕴）lIf a wff w has value True under all of interpretations for which each of the wffs in a set has value True, logically entails w and w logically follows from and w is a logical consequence of .le.g.P PP, P Q QF wP Q P1913.6 Soundness and CompletenesslIf, for any set of wffs, , and wf

20、f, w, R w implies w, the set of inference rules, R, is sound （合理）.lIf, for any set of wffs, , and wff, w, it is the case that whenever w, there exist a proof of w from using the set of inference rules, we say that R is complete.lWhen inference rules are sound and complete, we can determine whether o

21、ne wff follows from a set of wffs by searching for a proof.2013.6 Soundness and CompletenesslWhen the inference rules are sound, if we can find a proof of w from , w logically follows from .lWhen the inference rules are complete, we will eventually be able to confirm that w follows from by using a c

22、omplete search procedure to search for a proof.lTo determine whether or not a wff logically follows from a set of wffs or can be proved from a set of wffs is, in general, an NP-hard problem.2113.7 The PSAT ProblemlPropositional satisfiability (PSAT) problem: The problem of finding a model for a form

23、ula.lClauseA disjunction of literalslConjunctive Normal Form (CNF)A formula written as a conjunction of clauseslAn exhaustive procedure for solving the CNF PSAT problem is to try systematically all of the ways to assign True and False to the atoms in the formula.If there are n atoms in the formula,

24、there are 2n different assignments.2213.7 The PSAT ProblemlInteresting Special Cases2SAT and 3SATkSAT problemlTo find a model for a conjunction of clauses, the longest of which contains exactly k literals2SATlPolynomial complexity3SATlNP-completeMany problems take only polynomial expected time.2313.

25、7 The PSAT ProblemlGSATNonexhaustive, greedy, hill-climbing type of search procedureBegin by selecting a random set of values for all of the atoms in the formula.lThe number of clauses having value True under this interpretation is noted.Next, go through the list of atoms and calculate, for each one

26、, the increase in the number of clauses whose values would be True if the value of that atom were to be changed.lChange the value of that atom giving the largest increaselTerminated after some fixed number of changeslMay terminate at a local maximum2413.8.2 Metatheorems（元定理）元定理）lTheorems about the propositional calculuslImportant ThoremsDeductive theoremlIf w1, w2, , wn w, (w1 w2 wn) w is valid.Reducio ad absurdum（反证法）lIf the set has a model but w does not, then w.