logo

Giáo trình trí tuệ nhân tạo- phần 2- chương 5-Tri thức và lập luận - Logic mệnh đề

Trong chương này chúng ta sẽ trình bày các đặc trưng của ngôn ngữ biểu diễn tri thức. Chúng ta sẽ nghiên cứu logic mệnh đề, một ngôn ngữ biểu diễn tri thức rất đơn giản, có khả năng biểu diễn hẹp, nhưng thuận lợi cho ta làm quen với nhiều khái niệm quan trọng trong logic, đặc biệt trong logic vị từ cấp một sẽ được nghiên cứu trong các chương sau.
PhÇn II Tri thøc vµ lËp luËn ------------------------------------------ Ch¬ng 5. Logic mÖnh ®Ò Trong ch¬ng nµy chóng ta sÏ tr×nh bµy c¸c ®Æc trng cña ng«n ng÷ biÓu diÔn tri thøc. Chóng ta sÏ nghiªn cøu logic mÖnh ®Ò, mét ng«n ng÷ biÓu diÔn tri thøc rÊt ®¬n gi¶n, cã kh¶ n¨ng biÓu diÔn hÑp, nhng thuËn lîi cho ta lµm quen víi nhiÒu kh¸i niÖm quan träng trong logic, ®Æc biÖt trong logic vÞ tõ cÊp mét sÏ ®îc nghiªn cøu trong c¸c ch¬ng sau. 5.1. BiÓu diÔn tri thøc Con ngêi sèng trong m«i trêng cã thÓ nhËn thøc ®îc thÕ giíi nhê c¸c gi¸c quan (tai, m¾t vµ c¸c bé phËn kh¸c), sö dông c¸c tri thøc tÝch luü ®îc vµ nhê kh¶ n¨ng lËp luËn, suy diÔn, con ngêi cã thÓ ®a ra c¸c hµnh ®éng hîp lý cho c«ng viÖc mµ con ngêi ®ang lµm. Mét môc tiªu cña TrÝ tuÖ nh©n t¹o øng dông lµ thiÕt kÕ c¸c t¸c nh©n th«ng minh (intelligent agent) còng cã kh¶ n¨ng ®ã nh con ngêi. Chóng ta cã thÓ hiÓu t¸c nh©n th«ng minh lµ bÊt cø c¸i g× cã thÓ nhËn thøc ®îc m«i trêng th«ng qua c¸c bé c¶m nhËn (sensors) vµ ®a ra hµnh ®éng hîp lý ®¸p øng l¹i m«i trêng th«ng qua bé phËn hµnh ®éng (effectors). C¸c robots, c¸c softbot (software robot), c¸c hÖ chuyªn gia,... lµ c¸c vÝ dô vÒ t¸c nh©n th«ng minh. C¸c t¸c nh©n th«ng minh cÇn ph¶i cã tri thøc vÒ thÕ giíi hiÖn thùc míi cã thÓ ®a ra c¸c quyÕt ®Þnh ®óng ®¾n. Thµnh phÇn trung t©m cña c¸c t¸c nh©n dùa trªn tri thøc (knowledge-based agent), cßn ®îc gäi lµ hÖ dùa trªn tri thøc (knowledge-based system) hoÆc ®¬n gi¶n lµ hÖ tri thøc, lµ c¬ së tri thøc. C¬ së tri thøc (CSTT) lµ mét tËp hîp c¸c tri thøc ®îc biÓu diÔn díi d¹ng nµo ®ã. Mçi khi nhËn ®îc c¸c th«ng tin ®a vµo, t¸c nh©n cÇn cã kh¶ n¨ng suy diÔn ®Ó ®a ra c¸c c©u tr¶ lêi, c¸c hµnh ®éng hîp lý, ®óng ®¾n. NhiÖm vô nµy ®îc thùc hiÖn bëi bé suy diÔn. Bé suy diÔn lµ thµnh phÇn c¬ b¶n kh¸c cña c¸c hÖ tri thøc. Nh vËy hÖ tri thøc b¶o tr× mét CSTT vµ ®îc trang bÞ mét thñ tôc suy diÔn. Mçi khi tiÕp nhËn ®îc c¸c sù kiÖn tõ m«i trêng, thñ tôc suy diÔn thùc hiÖn qu¸ tr×nh liªn kÕt c¸c sù kiÖn víi c¸c tri thøc trong CSTT ®Ó rót ra c¸c c©u tr¶ lêi, hoÆc c¸c hµnh ®éng hîp lý mµ t¸c nh©n cÇn thùc hiÖn. §¬ng nhiªn lµ, khi ta thiÕt kÕ mét t¸c nh©n gi¶i quyÕt mét vÊn ®Ò nµo ®ã th× CSTT sÏ chøa c¸c tri thøc vÒ miÒn ®èi tîng cô thÓ ®ã. §Ó m¸y tÝnh cã thÓ sö dông ®îc tri thøc, cã thÓ xö lý tri thøc, chóng ta cÇn biÓu diÔn tri thøc díi d¹ng thuËn tiÖn cho m¸y tÝnh. §ã lµ môc tiªu cña biÓu diÔn tri thøc. Tri thøc ®îc m« t¶ díi d¹ng c¸c c©u trong ng«n ng÷ biÓu diÔn tri thøc. Mçi c©u cã thÓ xem nh sù m· hãa cña mét sù hiÓu biÕt cña chóng ta vÒ thÕ giíi hiÖn thùc. Ng«n ng÷ biÓu diÔn tri thøc (còng nh mäi ng«n ng÷ h×nh thøc kh¸c) gåm hai thµnh phÇn c¬ b¶n lµ có ph¸p vµ ng÷ nghÜa. 1 • Có ph¸p cña mét ng«n ng÷ bao gåm c¸c ký hiÖu vÒ c¸c quy t¾c liªn kÕt c¸c ký hiÖu (c¸c luËt có ph¸p) ®Ó t¹o thµnh c¸c c©u (c«ng thøc) trong ng«n ng÷. C¸c c©u ë ®©y lµ biÓu diÔn ngoµi, cÇn ph©n biÖt víi biÓu diÔn bªn trong m¸y tÝnh. C¸c c©u sÏ ®- îc chuyÓn thµnh c¸c cÊu tróc d÷ liÖu thÝch hîp ®îc cµi ®Æt trong mét vïng nhí nµo ®ã cña m¸y tÝnh, ®ã lµ biÓu diÔn bªn trong. B¶n th©n c¸c c©u cha chøa ®ùng mét néi dung nµo c¶, cha mang mét ý nghÜa nµo c¶. • Ng÷ nghÜa cña ng«n ng÷ cho phÐp ta x¸c ®Þnh ý nghÜa cña c¸c c©u trong mét miÒn nµo ®ã cña thÕ giíi hiÖn thùc. Ch¼ng h¹n, trong ng«n ng÷ c¸c biÓu thøc sè häc, d·y ký hiÖu (x+y)*z lµ mét c©u viÕt ®óng có ph¸p. Ng÷ nghÜa cña ng«n ng÷ nµy cho phÐp ta hiÓu r»ng, nÕu x, y, z, øng víi c¸c sè nguyªn, ký hiÖu + øng víi phÐp to¸n céng, cßn * øng víi phÐp chia, th× biÓu thøc (x+y)*z biÓu diÔn qu¸ tr×nh tÝnh to¸n: lÊy sè nguyªn x céng víi sè nguyªn y, kÕt qu¶ ®îc nh©n víi sè nguyªn z. • Ngoµi hai thµnh phÇn có ph¸p vµ ng÷ nghÜa, ng«n ng÷ biÓu diÔn tri thøc cÇn ®îc cung cÊp c¬ chÕ suy diÔn. Mét luËt suy diÔn (rule of inference) cho phÐp ta suy ra mét c«ng thøc tõ mét tËp nµo ®ã c¸c c«ng thøc. Ch¼ng h¹n, trong logic mÖnh ®Ò, luËt modus ponens tõ hai c«ng thøc A vµ A⇒B suy ra c«ng thøc B. Chóng ta sÏ hiÓu lËp luËn hoÆc suy diÔn lµ mét qu¸ tr×nh ¸p dông c¸c luËt suy diÔn ®Ó tõ c¸c tri thøc trong c¬ së tri thøc vµ c¸c sù kiÖn ta nhËn ®îc c¸c tri thøc míi. Nh vËy chóng ta x¸c ®Þnh: Ng«n ng÷ biÓu diÔn tri thøc = Có ph¸p + Ng÷ nghÜa + C¬ chÕ suy diÔn. Mét ng«n ng÷ biÓu diÔn tri thøc tèt cÇn ph¶i cã kh¶ n¨ng biÓu diÔn réng, tøc lµ cã thÓ m« t¶ ®îc mäi ®iÒu mµ chóng ta muèn nãi. Nã cÇn ph¶i hiÖu qu¶ theo nghÜa lµ, ®Ó ®i tíi c¸c kÕt luËn, thñ tôc suy diÔn ®ßi hái Ýt thêi gian tÝnh to¸n vµ Ýt kh«ng gian nhí. Ngêi ta còng mong muèn ng«n ng÷ biÓu diÔn tri thøc gÇn víi ng«n ng÷ tù nhiªn. Trong s¸ch nµy, chóng ta sÏ tËp trung nghiªn cøu logic vÞ tõ cÊp mét (first-order predicate logic hoÆc first-order predicate calculus) - mét ng«n ng÷ biÓu diÔn tri thøc, bëi v× logic vÞ tõ cÊp mét cã kh¶ n¨ng biÓu diÔn t¬ng ®èi tèt, vµ h¬n n÷a nã lµ c¬ së cho nhiÒu ng«n ng÷ biÓu diÔn tri thøc kh¸c, ch¼ng h¹n to¸n hoµn c¶nh (situation calculus) hoÆc logic thêi gian kho¶ng cÊp mét (first-order interval tempral logic). Nhng tríc hÕt chóng ta sÏ nghiªn cøu logic mÖnh ®Ò (propositional logic hoÆc propositional calculus). Nã lµ ng«n ng÷ rÊt ®¬n gi¶n, cã kh¶ n¨ng biÓu diÔn h¹n chÕ, song thuËn tiÖn cho ta ®a vµo nhiÒu kh¸i niÖm quan träng trong logic. 5.2. Có ph¸p vµ ng÷ nghÜa cña logic mÖnh ®Ò. 5.2.1 Có ph¸p: Có ph¸p cña logic mÖnh ®Ò rÊt ®¬n gi¶n, nã cho phÐp x©y dùng nªn c¸c c«ng thøc. Có ph¸p cña logic mÖnh ®Ò bao gåm tËp c¸c ký hiÖu vµ tËp c¸c luËt x©y dùng c«ng thøc. 1. C¸c ký hiÖu • Hai h»ng logic True vµ False. • C¸c ký hiÖu mÖnh ®Ò (cßn ®îc gäi lµ c¸c biÕn mÖnh ®Ò): P, Q,... • C¸c kÕt nèi logic ∧, ∨, , ⇒, ⇔. • C¸c dÊu më ngoÆc (vµ ®ãng ngoÆc). 2 2. C¸c quy t¾c x©y dùng c¸c c«ng thøc • C¸c biÕn mÖnh ®Ò lµ c«ng thøc. • NÕu A vµ B lµ c«ng thøc th×: (A∧B) (®äc “A héi B” hoÆc “A vµ B”) (A∨B) (®äc “A tuyÓn B” hoÆc “A hoÆc B”) (A) (®äc “phñ ®Þnh A”) (A⇒B) (®äc “A kÐo theo B” hoÆc “nÕu A th× B”) (A⇔B) (®äc “A vµ B kÐo theo nhau”) lµ c¸c c«ng thøc. Sau nµy ®Ó cho ng¾n gän, ta sÏ bá ®i c¸c cÆp dÊu ngoÆc kh«ng cÇn thiÕt. Ch¼ng h¹n, thay cho ((A∨B)∧C) ta sÏ viÕt lµ (A∨B)∧C. C¸c c«ng thøc lµ c¸c ký hiÖu mÖnh ®Ò sÏ ®îc gäi lµ c¸c c©u ®¬n hoÆc c©u ph©n tö. C¸c c«ng thøc kh«ng ph¶i lµ c©u ®¬n sÏ ®îc gäi lµ c©u phøc hîp. NÕu P lµ ký hiÖu mÖnh ®Ò th× P vµ TP ®îc gäi lµ literal, P lµ literal d¬ng, cßn TP lµ literal ©m. C©u phøc hîp cã d¹ng A1∨...∨Am trong ®ã Ai lµ c¸c literal sÏ ®îc gäi lµ c©u tuyÓn (clause). 5.2.2 Ng÷ nghÜa: Ng÷ nghÜa cña logic mÖnh ®Ò cho phÐp ta x¸c ®Þnh thiÕt lËp ý nghÜa cña c¸c c«ng thøc trong thÕ giíi hiÖn thùc nµo ®ã. §iÒu ®ã ®îc thùc hiÖn b»ng c¸ch kÕt hîp mÖnh ®Ò víi sù kiÖn nµo ®ã trong thÕ giíi hiÖn thùc. Ch¼ng h¹n, ký hiÖu mÖnh ®Ò P cã thÓ øng víi sù kiÖn “Paris lµ thñ ®« níc Ph¸p” hoÆc bÊt kú mét sù kiÖn nµo kh¸c. BÊt kú mét sù kÕt hîp c¸c kÝ hiÖu mÖnh ®Ò víi c¸c sù kiÖn trong thÕ giíi thùc ®îc gäi lµ mét minh häa (interpretation ). Ch¼ng h¹n minh häa cña kÝ hiÖu mÖnh ®Ò P cã thÓ lµ mét sù kiÖn (mÖnh ®Ò) “Paris lµ thñ ®« níc Ph¸p ”. Mét sù kiÖn chØ cã thÓ ®óng hoÆc sai. Ch¼ng h¹n, sù kiÖn “Paris lµ thñ ®« níc Ph¸p ” lµ ®óng, cßn sù kiÖn “Sè Pi lµ sè h÷u tØ ” lµ sai. Mét c¸ch chÝnh x¸c h¬n, cho ta hiÓu mét minh häa lµ mét c¸ch g¸n cho mçi ký hiÖu mÖnh ®Ò mét gi¸ trÞ ch©n lý True hoÆc False. Trong mét minh häa, nÕu kÝ hiÖu mÖnh ®Ò P ®îc g¸n gi¸ trÞ ch©n lý True/False (P nghÜa cña phÐp kÐo theo P => Q (P kÐo theo Q ), P lµ gi¶ thiÕt, cßn Q lµ kÕt luËn. Trùc quan cho phÐp ta xem r»ng, khi P lµ ®óng vµ Q lµ ®óng th× c©u “P kÐo theo Q ” lµ ®óng, cßn khi P lµ ®óng Q lµ sai th× c©u “P kÐo theo Q” lµ sai. Nhng nÕu P sai vµ Q ®óng , hoÆc P sai Q sai th× “P kÐo theo Q” lµ ®óng hay sai ? NÕu chóng ta xuÊt ph¸t tõ gi¶ thiÕt sai, th× chóng ta kh«ng thÓ kh¶ng ®Þnh g× vÒ kÕt luËn. Kh«ng cã lý do g× ®Ó nãi r»ng, nÕu P sai vµ Q ®óng hoÆc P sai vµ Q sai th× “P kÐo theo Q” lµ sai. Do ®ã trong trêng hîp P sai th× “P kÐo theo Q ” lµ ®óng dï Q lµ ®óng hay Q lµ sai. B¶ng ch©n lý cho phÐp ta x¸c ®Þnh ngÉu nhiªn c¸c c©u phøc hîp. Ch¼ng h¹n ng÷ nghÜa cña c¸c c©u P∧Q trong minh häa {P kh«ng b»ng ph¬ng ph¸p b¶ng ch©n lý, ®ßi hái thêi gian mò. Cook (1971) ®· chøng minh r»ng, vÊn ®Ò kiÓm tra mét c«ng thøc trong logic mÖnh ®Ò cã tho¶ ®îc hay kh«ng lµ vÊn ®Ò NP-®Çy ®ñ. Chóng ta sÏ nãi r»ng (tho¶ ®îc, kh«ng tho¶ ®îc) nÕu héi cña chóng G1∧.......∧Gm lµ v÷ng ch¾c (tho¶ ®îc, kh«ng tho¶ ®îc). Mét m« h×nh cña tËp c«ng thøc G lµ m« h×nh cña tËp c«ng thøc G1∧.......∧Gm . 5.3 D¹ng chuÈn t¾c Trong môc nµy chóng ta sÏ xÐt viÖc chuÈn hãa c¸c c«ng thøc, ®a c¸c c«ng thøc vÒ d¹ng thuËn lîi cho viÖc lËp luËn, suy diÔn. Tríc hÕt ta sÏ xÐt c¸c phÐp biÕn ®æi t- ¬ng ®¬ng. Sö dông c¸c phÐp biÓn ®æi nµy, ta cã thÓ ®a mét c«ng thøc bÊt kú vÒ c¸c d¹ng chuÈn t¾c. 5.3.1 Sù t¬ng ®¬ng cña c¸c c«ng thøc Hai c«ng thøc A vµ B ®îc xem lµ t¬ng ®¬ng nÕu chóng cã cïng mét gi¸ trÞ ch©n lý trong mäi minh häa. §Ó chØ A t¬ng ®¬ng víi B ta viÕt A≡ B b»ng ph¬ng ph¸p b¶ng ch©n lý, dÔ dµng chøng minh ®îc sù t¬ng ®¬ng cña c¸c c«ng thøc sau ®©y : • A=>B ≡ lA v B • A< = > B ≡ (A=>B) ∧ (B=>A) • l(lA) ≡A LuËt De Morgan • l(A v B) ≡ lA ∧ lB • l(A ∧ B) ≡ lA v lB LuËt giao ho¸n • AvB ≡BvA • A∧B ≡B∧A LuËt kÕt hîp • (A v B) v C ≡ Av( B v C) • (A ∧ B) ∧ C ≡ A∧ ( B ∧ C) LuËt ph©n phèi • A ∧ (B v C) ≡ (A ∧ B ) v (A ∧ C) • A v (B ∧ C) ≡ (A v B ) ∧ (A v C) 5.3.2 D¹ng chuÈn t¾c : C¸c c«ng thøc t¬ng ®¬ng cã thÓ xem nh c¸c biÓu diÔn kh¸c nhau cña cïng mét sù kiÖn. §Ó dÔ dµng viÕt c¸c ch¬ng tr×nh m¸y tÝnh thao t¸c trªn c¸c c«ng thøc, chóng ta sÏ chuÈn hãa c¸c c«ng thøc, ®a chóng vÒ d¹ng biÓu diÔn chuÈn ®îc gäi lµ d¹ng chuÈn héi. Mét c«ng thøc ë d¹ng chuÈn héi, cã d¹ng A1 v ... .v Am trong ®ã c¸c Ai lµ literal . Chóng ta cã thÓ biÕn ®æi mét c«ng thøc bÊt kú vÒ c«ng thøc ë d¹ng chuÈn héi b»ng c¸ch ¸p dông c¸c thñ tôc sau. 5 • Bá c¸c dÊu kÐo theo (=>) b»ng c¸ch thay (A=>B) bëi (lAvB). • ChuyÓn c¸c dÊu phñ ®Þnh (l) vµo s¸t c¸c kÝ hiÖu mÖnh ®Ò b»ng c¸ch ¸p dông luËt De Morgan vµ thay l(lA) bëi A . • ¸p dông luËt ph©n phèi, thay c¸c c«ng thøc cã d¹ng Av(B∧C) bëi (A v B) ∧ ( A vB). VÝ dô : Ta chuÈn hãa c«ng thøc ( P => Q) v l(R v lS) : (P => Q) v l(R v lS) ≡ (lP v Q) v (lR ∧ S) ≡ ((lP v Q)vlR) ∧ ( (lP v Q) v S) ≡ (l P v Q v lR) ∧ (lP v Q v S). Nh vËy c«ng thøc (P=> Q) v l(R v lS) ®îc ®a vÒ d¹ng chuÈn héi (lP v Q v lR) ∧ (lP v Q v S). Khi biÓu diÔn tri thøc bëi c¸c c«ng thøc trong logic mÖnh ®Ò, c¬ së tri thøc lµ mét tËp nµo ®ã c¸c c«ng thøc. B»ng c¸ch chuÈn ho¸ c¸c c«ng thøc, c¬ së tri thøc lµ mét tËp nµo ®ã c¸c c©u tuyÓn. C¸c c©u Horn: ë trªn ta ®· chØ ra, mäi c«ng thøc ®Òu cã thÓ ®a vÒ d¹ng chuÈn héi, tøc lµ c¸c héi cña c¸c tuyÓn, mçi c©u tuyÓn cã d¹ng lP1 v........v lPm v Q1 v.....v Qm trong ®ã Pi , Qi lµ c¸c ký hiÖu mÖnh ®Ò (literal d¬ng) c©u nµy t¬ng ®¬ng víi c©u lP1 v........v lPm => v Q1 v.....v Qm D¹ng c©u nµy ®îc gäi lµ c©u Kowalski (do nhµ logic Kowalski ®a ra n¨m 1971). Khi n 0, n=1, c©u Horn cã d¹ng : P1 ∧.....∧ Pm => Q Trong ®ã Pi , Q lµ c¸c literal d¬ng. C¸c Pi ®îc gäi lµ c¸c ®iÒu kiÖn (hoÆc gi¶ thiÕt), cßn Q ®îc gäi lµ kÕt luËn (hoÆc hÖ qu¶ ). C¸c c©u Horn d¹ng nµy cßn ®îc gäi lµ c¸c luËt if ... then vµ ®îc biÓu diÔn nh sau : If P1 and ....and Pm then Q . Khi m=0, n=1 c©u Horn trë thµnh c©u ®¬n Q, hay sù kiÖn Q. NÕu m>0, n=0 c©u Horn trë thµnh d¹ng lP1 v......v lPm hay t¬ng ®¬ng l(P1v...v Pm ). CÇn chó ý r»ng, kh«ng ph¶i mäi c«ng thøc ®Òu cã thÓ biÓu diÔn díi d¹ng héi cña c¸c c©u Horn. Tuy nhiªn trong c¸c øng dông, c¬ së tri thøc thêng lµ mét tËp nµo ®ã c¸c c©u Horn (tøc lµ mét tËp nµo ®ã c¸c luËt if-then). 5.4 LuËt suy diÔn Mét c«ng thøc H ®îc xem lµ hÖ qña logic (logical consequence) cña mét tËp c«ng thøc G ={G1,.....,Gm} nÕu trong bÊt kú minh häa nµo mµ {G 1,.....,Gm} ®óng th× H còng ®óng, hay nãi c¸ch kh¸c bÊt kú mét m« h×nh nµo cña G còng lµ m« h×nh cña H. Khi cã mét c¬ së tri thøc, ta muèn sö dông c¸c tri thøc trong c¬ së nµy ®Ó suy ra tri thøc míi mµ nã lµ hÖ qu¶ logic cña c¸c c«ng thøc trong c¬ së tri thøc. §iÒu ®ã ®îc thùc hiÖn b»ng c¸c thùc hiÖn c¸c luËt suy diÔn (rule of inference). LuËt suy diÔn gièng nh mét thñ tôc mµ chóng ta sö dông ®Ó sinh ra mét c«ng thøc míi tõ c¸c c«ng thøc ®· cã. Mét luËt suy diÔn gåm hai phÇn : mét tËp c¸c ®iÒu kiÖn vµ mét kÕt luËn. Chóng ta sÏ biÓu diÔn c¸c luËt suy diÔn díi d¹ng “ph©n sè ”, trong ®ã tö sè lµ danh s¸ch c¸c ®iÒu 6 kiÖn, cßn mÉu sè lµ kÕt luËn cña luËt, tøc lµ mÉu sè lµ c«ng thøc míi ®îc suy ra tõ c¸c c«ng thøc ë tö sè. Sau ®©y lµ mét sè luËt suy diÔn quan träng trong logic mÖnh ®Ò. Trong c¸c luËt nµy α, αi , β, γ lµ c¸c c«ng thøc : • LuËt Modus Ponens α=>β,α β Tõ mét kÐo theo vµ gi¶ thiÕt cña kÐo theo, ta suy ra kÕt luËn cña nã. • LuËt Modus Tollens α=>β,lβ lα Tõ mét kÐo theo vµ phñ ®Þnh kÕt luËn cña nã, ta suy ra phñ ®Þnh gi¶ thiÕt cña kÐo theo. • LuËt b¾c cÇu α=>β,β=>γ α=>γ Tõ hai kÐo theo, mµ kÕt luËn cña nã lµ cña kÐo theo thø nhÊt trïng víi gi¶ thiÕt cña kÐo theo thø hai, ta suy ra kÐo theo míi mµ gi¶ thiÕt cña nã lµ gi¶ thiÕt cña kÐo theo thø nhÊt, cßn kÕt luËn cña nã lµ kÕt luËn cña kÐo theo thø hai. • LuËt lo¹i bá héi α1∧.......∧αi∧........∧αm αi Tõ mét héi ta ®a ra mét nh©n tö bÊt kú cña héi . • LuËt ®a vµo héi α1,.......,αi,........αm α1∧.......∧αi∧....... ∧αm Tõ mét danh s¸ch c¸c c«ng thøc, ta suy ra héi cña chóng. • LuËt ®a vµo tuyÓn αi α1v.......vαi.v.......vαm Tõ mét c«ng thøc, ta suy ra mét tuyÓn mµ mét trong c¸c h¹ng tö cña c¸c tuyÓn lµ c«ng thøc ®ã. • LuËt gi¶i α v β,lβ v γ αvγ Tõ hai tuyÓn, mét tuyÓn chøa mét h¹ng tö ®èi lËp víi mét h¹ng tö trong tuyÓn kia, ta suy ra tuyÓn cña c¸c h¹ng tö cßn l¹i trong c¶ hai tuyÓn. Mét luËt suy diÔn ®îc xem lµ tin cËy (secured) nÕu bÊt kú mét m« h×nh nµo cña gi¶ thiÕt cña luËt còng lµ m« h×nh kÕt luËn cña luËt. Chóng ta chØ quan t©m ®Õn c¸c luËt suy diÔn tin cËy. B»ng ph¬ng ph¸p b¶ng ch©n lý, ta cã thÓ kiÓm chøng ®îc c¸c luËt suy diÔn nªu trªn ®Òu lµ tin cËy. B¶ng ch©n lý cña luËt gi¶i ®îc cho trong h×nh 5.3. Tõ b¶ng nµy ta 7 thÊy r»ng, trong bÊt kú mét minh häa nµo mµ c¶ hai gi¶ thiÕt α v β, lβ v γ ®óng th× kÕt luËn α v γ còng ®óng. Do ®ã luËt gi¶i lµ luËt suy ®iÔn tin cËy. α β γ αvβ lβ v γ αvγ False False False False True False False False True False True True False True False True False False False True True True True True True False False True True True True False True True True True True True False True False True True True True True True True H×nh 5.3 B¶ng ch©n lý chøng minh tÝnh tin cËy cña luËt gi¶i. Ta cã nhËn xÐt r»ng, luËt gi¶i lµ mét luËt suy diÔn tæng qu¸t, nã bao gåm luËt Modus Ponens, luËt Modus Tollens, luËt b¾c cÇu nh c¸c trêng hîp riªng. (B¹n ®äc dÔ dµng chøng minh ®îc ®iÒu ®ã). Tiªn ®Ò ®Þnh lý chøng minh. Gi¶ sö chóng ta cã mét tËp nµo ®ã c¸c c«ng thøc. C¸c luËt suy diÔn cho phÐp ta tõ c¸c c«ng thøc ®· cã suy ra c«ng thøc míi b»ng mét d·y ¸p dông c¸c luËt suy diÔn. C¸c c«ng thøc ®· cho ®îc gäi lµ c¸c tiªn ®Ò . C¸c c«ng thøc ®îc suy ra ®îc gäi lµ c¸c ®Þnh lý. D·y c¸c luËt ®îc ¸p dông ®Ó dÉn tíi ®Þnh lý ®îc gäi lµ mét chøng minh cña ®Þnh lý. NÕu c¸c luËt suy diÔn lµ tin cËy, th× c¸c ®Þnh lý lµ hÖ qu¶ logic cña c¸c tiªn ®Ò. VÝ dô: Gi¶ sö ta cã c¸c c«ng thøc sau : Q ∧ S => G v H (1) P => Q (2) R => S (3) P (4) R (5) Tõ c«ng thøc (2) vµ (4), ta suy ra Q (LuËt Modus Ponens) . L¹i ¸p dông luËt Modus Ponens, tõ (3) vµ (5) ta suy ra S . Tõ Q, S ta suy ra Q ∧S (luËt ®a vµo héi ). Tõ (1) vµ Q∧S ta suy ra G v H. C«ng thøc G v H ®· ®îc chøng minh. Trong c¸c hÖ tri thøc, ch¼ng h¹n c¸c hÖ chuyªn gia, hÖ lËp tr×nh logic,..., sö dông c¸c luËt suy diÔn ngêi ta thiÕt kÕ lªn c¸c thñ tôc suy diÔn (cßn ®îc gäi lµ thñ tôc chøng minh) ®Ó tõ c¸c tri thøc trong c¬ së tri thøc ta suy ra c¸c tri thøc míi ®¸p øng nhu cÇu cña ngêi sö dông. Mét hÖ h×nh thøc (formal system) bao gåm mét tËp c¸c tiªn ®Ò vµ mét tËp c¸c luËt suy diÔn nµo ®ã (trong ng«n ng÷ biÓu diÔn tri thøc nµo ®ã ). Mét tËp luËt suy diÔn ®îc xem lµ ®Çy ®ñ, nÕu mäi hÖ qu¶ logic cña mét tËp c¸c tiªn ®Ò ®Òu chøng minh ®îc b»ng c¸ch chØ sö dông c¸c luËt cña tËp ®ã. Ph¬ng ph¸p chøng minh b¸c bá Ph¬ng ph¸p chøng minh b¸c bá (refutation proof hoÆc proof by contradiction) lµ mét ph¬ng ph¸p thêng xuyªn ®îc sö dông trong c¸c chøng minh to¸n häc. T tëng cña ph¬ng ph¸p nµy lµ nh sau : §Ó chøng minh P ®óng, ta gi¶ sö P sai ( thªm  P vµo c¸c gi¶ thiÕt ) vµ dÉn tíi mét m©u thuÉn. Sau ®©y ta sÏ tr×nh bÇy c¬ së nµy. 8 Gi¶ sö chóng ta cã mét tËp hîp c¸c c«ng thøc G ={G1,.....,Gm} ta cÇn chøng minh c«ng thøc H lµ hÖ qu¶ logic cña G . §iÒu ®ã t¬ng ®¬ng víi chøng minh c«ng thøc G1^....^Gm -> H lµ v÷ng ch¾c. Thay cho chøng minh G 1^..... ^Gm =>H lµ v÷ng ch¾c, ta chøng minh G1^....^Gm ^ H lµ kh«ng tháa m·n ®îc. Tøc lµ ta chøng minh tËp G’‘= ( G1,.......,Gm, H ) lµ kh«ng tháa ®îc nÕu tõ G‘ta suy ra hai mÖnh ®Ò ®èi lËp nhau. ViÖc chøng minh c«ng thøc H lµ hÖ qu¶ logic cña tËp c¸c tiªu ®Ò G b»ng c¸ch chøng minh tÝnh kh«ng tháa ®îc cña tËp c¸c tiªu ®Ò ®îc thªm vµo phñ ®Þnh cña c«ng thøc cÇn chøng minh, ®îc gäi lµ chøng minh b¸c bá. 5.5 LuËt gi¶i, chøng minh b¸c bá b»ng luËt gi¶i §Ó thuËn tiÖn cho viÖc sö dông luËt gi¶i, chóng ta sÏ cô thÓ ho¸ luËt gi¶i trªn c¸c d¹ng c©u ®Æc biÖt quan träng. • LuËt gi¶i trªn c¸c c©u tuyÓn A1 v. . ............. vAm v C  C v B1 v.. ............. v Bn A1 v.. ......... v Am v B1 v.... v Bn trong ®ã Ai, Bj vµ C lµ c¸c literal. • LuËt gi¶i trªn c¸c c©u Horn: Gi¶ sö Pi, Rj, Q vµ S lµ c¸c literal. Khi ®ã ta cã c¸c luËt sau : P1 ^. ..............^Pm ^ S => Q, R1 ^. .............^ Rn => S P1 ^........^Pm ^ R1 ^...... ^ Rn =>Q Mét trêng hîp riªng hay ®îc sö dông cña luËt trªn lµ : P1 ^...............^ Pm ^ S => Q, S P1 ^................^Pm => Q Khi ta cã thÓ ¸p dông luËt gi¶i cho hai c©u, th× hai c©u nµy ®îc gäi lµ hai c©u gi¶i ®îc vµ kÕt qu¶ nhËn ®îc khi ¸p dông luËt gi¶i cho hai c©u ®ã ®îc gäi lµ gi¶i thøc cña chóng. Gi¶i thøc cña hai c©u A vµ B ®îc kÝ hiÖu lµ res(A,B). Ch¼ng h¹n, hai c©u tuyÓn gi¶i ®îc nÕu mét c©u chøa mét literal ®èi lËp víi mét literal trong c©u kia. Gi¶i thøc cña hai literal ®èi lËp nhau (P vµ  P) lµ c©u rçng, chóng ta sÏ ký hiÖu c©u rçng lµ [] , c©u rçng kh«ng tho¶ ®îc. Gi¶ sö G lµ mét tËp c¸c c©u tuyÓn ( B»ng c¸ch chuÈn ho¸ ta cã thÓ ®a mét tËp c¸c c«ng thøc vÒ mét tËp c¸c c©u tuyÓn ). Ta sÏ ký hiÖu R(G ) lµ tËp c©u bao gåm c¸c c©u thuéc G vµ tÊt c¶ c¸c c©u nhËn ®îc tõ G b»ng mét d·y ¸p dông luËt gi¶i. LuËt gi¶i lµ luËt ®Çy ®ñ ®Ó chøng minh mét tËp c©u lµ kh«ng tháa ®îc. §iÒu nµy ®îc suy tõ ®Þnh lý sau : §Þnh lý gi¶i: Mét tËp c©u tuyÓn lµ kh«ng tháa ®îc nÕu vµ chØ nÕu c©u rçng [] ∈ R(G ). §Þnh lý gi¶i cã nghÜa r»ng, nÕu tõ c¸c c©u thuéc G , b»ng c¸ch ¸p dông luËt gi¶i ta dÉn tíi c©u rçng th× G lµ kh«ng tháa ®îc, cßn nÕu kh«ng thÓ sinh ra c©u rçng b»ng luËt gi¶i th× G tháa ®îc. Lu ý r»ng, viÖc dÉn tíi c©u rçng cã nghÜa lµ ta ®· dÉn tíi hai literal ®èi lËp nhau P vµ  P ( tøc lµ dÉn tíi m©u thuÉn ). 9 Tõ ®Þnh lý gi¶i, ta ®a ra thñ tôc sau ®©y ®Ó x¸c ®Þnh mét tËp c©u tuyÓn G lµ tháa ®îc hay kh«ng . Thñ tôc nµy ®îc gäi lµ thñ tôc gi¶i. procedure Resolution ; Input : tËp G c¸c c©u tuyÓn ; begin 1.Repeat 1.1 Chän hai c©u A vµ B thuéc G ; 1.2 if A vµ B gi¶i ®îc then tÝnh Res ( A,B ) ; 1.3 if Res (A,B ) lµ c©u míi then thªm Res ( A,B ) vµo G ; until nhËn ®îc [] hoÆc kh«ng cã c©u míi xuÊt hiÖn ; 2. if nhËn ®îc c©u rçng then th«ng b¸o G kh«ng tho¶ ®îc e lse th«ng b¸o G tho¶ ®îc ; end; Chóng ta cã nhËn xÐt r»ng, nÕu G lµ tËp h÷u h¹n c¸c c©u th× c¸c literal cã mÆt trong c¸c c©u cña G lµ h÷u h¹n. Do ®ã sè c¸c c©u tuyÓn thµnh lËp ®îc tõ c¸c literal ®ã lµ h÷u h¹n. V× vËy chØ cã mét sè h÷u h¹n c©u ®îc sinh ra b»ng luËt gi¶i. Thñ tôc gi¶i sÏ dõng l¹i sau mét sè h÷u h¹n bíc. ChØ sö dông luËt gi¶i ta kh«ng thÓ suy ra mäi c«ng thøc lµ hÖ qu¶ logic cña mét tËp c«ng thøc ®· cho. Tuy nhiªn, sö dông luËt gi¶i ta cã thÓ chøng minh ®îc mét c«ng thøc bÊt k× cã lµ hÖ qu¶ cña mét tËp c«ng thøc ®· cho hay kh«ng b»ng ph¬ng ph¸p chøng minh b¸c bá. V× vËy luËt gi¶i ®îc xem lµ luËt ®Çy ®ñ cho b¸c bá. Sau ®©y lµ thñ tôc chøng minh b¸c bá b»ng luËt gi¶i Procedure Refutation_Proof ; input : TËp G c¸c c«ng thøc ; C«ng thøc cÇn chøng minh H; Begin 1. Thªm H vµo G ; 2. ChuyÓn c¸c c«ng thøc trong G vÒ d¹ng chuÈn héi ; 3. Tõ c¸c d¹ng chuÈn héi ë bíc hai, thµnh lËp t¹p c¸c c©u tuyÓn g’ ; 4. ¸p dông thñ tôc gi¶i cho tËp c©u G’ ; 5. if G’ kh«ng tho¶ ®îc then th«ng b¸o H lµ hÖ qu¶ logic else th«ng b¸o H kh«ng lµ hÖ qu¶ logic cña G ; end; VÝ dô: Gi¶ giö G lµ tËp hîp c¸c c©u tuyÓn sau AvB v P (1) CvDv P (2) Ev C (3) A (4) E (5) D (6) Gi¶ sö ta cÇn chøng minh P. Thªm vµo G c©u sau: P (7) 10 ¸p dông luËt gi¶i cho c©u (2) vµ (7) ta ®îc c©u: CvD (8) Tõ c©u (6) vµ (8) ta nhËn ®îc c©u: C (9) Tõ c©u (3) vµ (9) ta nhËn ®îc c©u: E (10) Tíi ®©y ®· xuÊt hiÖn m©u thuÉn, v× c©u (5) vµ (10) ®èi lËp nhau. Tõ c©u (5) vµ (10) ta nhËn ®îc c©u rçng []. VËy P lµ hÖ qu¶ logic cña c¸c c©u (1) --(6). 11
DMCA.com Protection Status Copyright by webtailieu.net