استنتاج در منطق مرتبه اول: هوش مصنوعی

صفحه 1:


صفحه 2:
576 [17 eee art) 1. Modus 2. AUG’ = 1 0 Sorin © 30010 en 5-9 23 3. ۸60 - 4. 02- ‎Intrdduction‏ 1ع مه م0 ‎3 A, 4 ۸ 3 1 4 0 stag ig eae Ry Bok: ik © aM rea ¢ ah ‎Fae) is) ‏ا ا‎ 50 toy ‎37 01 ۰۰ 10 2 ۷ 

صفحه 3:
۳ ۱ gry) علامت فا ار ی SUBST( {x/hamid}, male(x) ) ‏ل‎ ‎like( Sam, Pam ) :0 ‏قرم زمينى‎ a ۲ —— ۲ Set eam ne Orek (Od) ead eee 

صفحه 4:
۱100 در منطق مرتيه اول ©3 سه قانون ل جدید: ‎OT eh a ۷ On eae A‏ برای هر جمله لا متفیر ۷ و ترم زمینی [ داریم: ۷ SUBST( {v/g} ; oa) Vx, Likes( x, icecream ) SUBST( {x/BEN} , Likes( BEN, icecream ) ) 

صفحه 5:
۱100 در منطق مرتيه اول ©3 2 حذف سور وجودعه ‎sa‏ لاك برای هر جمله لا ۰ متقیر ۷ و ثابت ک که جای دیگربایگاه دانش ظاهر نشده است دارئم: ‎aes‏ = SUBST( {v/K} , a) dx, Kill(x, victim ) 51851) {x/Murcerer} , Kill( Murderer , victim ) ) 

صفحه 6:
7 ae 7 3© ‏در منطق مرتيه اول‎ ۱1010 Cee ‏و‎ Cad ATCO Me re Seo) Stel ee et ee eee ioe ‏برای هر جمله‎ ras a dv, SUBST( {g/v} , a ) ‏لكا‎ ae eae) Sx thes (x | ioecreun ) (/7وز )1 )511851 با جانشينى ) 

صفحه 7:
۳23 01 ee YS) Generelined Modus Ponens ‏تعميم دافته‎ fey) ‏مودس‎ GMP ۳ 1 تعميمى از قانون استنتاج ‎And- Jls as Modus Ponens‏ 1 ‘ 1 حذف سور عمومى و 270126115 100115 است برای جملات اتمی :0 و :"0 و ) که برای تمامی ‎ES‏ ‏(رط,51785106 > ( ,100 5ظ1ا5 وجود دارد آنگاه: 2و0 ۳2۰۰۰۶ و۳ ۱ 75-0118 

صفحه 8:
فطل هشلتم: استئتاي در منطق مرتيه ‎LM‏ ‎Missile( M1)‏ منال: ‎Owns (NONO, M1)‏ ‎Yx Missile(x) “ owns( NONO , x) = sells( WEST ,‏ ‎NONO, x )‏ ا اللا ا ‎Fey‏ sells( WEST , NONO, SS M1 ) 9 ssl X Slo NONO 9 asl Sig0 GX guia aF Yisls olGl yo GX ish Rey pC ree LO) (Oren preerperorh | satay Mr Canyrrcnere ne rviny 

صفحه 9:
فصل هشنم: استنتاى در منطق مرتيه اول ۸ 0210000000 ۱۱ enn = NETS} ‏لست‎ ‏الس با تركيب تعدادى از استنتاج هاى كوجك و تبديل آن به يك استنتاج بزرك مراحل‎ زیادی را تقلیل می دهد 1 Fem were ea even ‏تصادفى سور عمومى) ضمانت مى شود. الكوريتم يكسان سازى دو جمله را مى كيرد‎ ‏و جانشينى ا در صورت وجود برميكرداند كه آن دو جمله يكسان شوند‎ فا این قانون تمام جملات موجود در بایگاه دانش وا به فرم کانونی در می آورد. انجام این عمل یکبار در مرحله آغازین. ما را از اتلاف زمان برای انجام تبدیلات در طول مرحله اثبات بی نیاز می کند 

صفحه 10:
۳۹ ۳ فصل هشّتم: استنتام در منطق مرتبه اول ‎ea‏ / فرم ‎Canonic‏ ‏ا ل ‎oe‏ ا ا ‎Fore oes eRe ce Psy Reel ee‏ ‎Revers ced Korn @31Y Bad‏ ا ا ل ‎ere ee nes cel pr eee‏ شرطي (با يك تركيب عطفي از جملات اتمي در طرف جب و يك اتم منفرد در طرف راست ‎ayer gic cams ie‏ ا ل ۱ پایگاه دانشی که ‎age ey Beng heey‏ الا الا ا ‎peep‏ Bee ما جمللات را به جمالات 010[ زمانی تبدیل می‌کنیم که ابتدا وارد پایگاه دانش, با استفاده از حذف سور وجودى وحذف 441101 شده باشند 3x Owns( Nono, x) “ Missile( x ) ‏منال:‎ ‎M1 ) Jjls oy5@ coil alee 99‏ )71/155116 تبديل می شود 

صفحه 11:
‎Py oo ۳۹‏ فصل ‎Tea Bere ewer ee)‏ يكسان سازى 1121202110 الگوریتم یکسان سازی دو جمله را می گیرد [1جانشینی را در صورت وجود برمیگردلند تا آن دو جمله يكسان شولك وظیفه روتین یکسان‌ساز ا جمله اتمي [) 10۰ و برگرداندن یک جانشین كه ]0 :2 را مشابه هم خواهد ساخت.. (اكر جنين جانشيني موجود نباشد. .101437 ‎Siri‏ برمي كرداند.» ‎UNIFY( p,q) = = (SUBST(6,p) =‏ ‎SUBST( 0,q ) a‏ ‎eee ae nel‏ له 111 عموميهرينزيكسارهبر 1721461 0626181 04056 يا ‏كعات كك رك ل ا ‎ere ee ence‏ كن ‎ey‏ ل ار 

صفحه 12:
3 [151۳ 0 0 “ John hates everyone he knows “ مى ار ‎ge‏ كني كد ‎oa (0) 2801‏ 000000 ol, Knows( John, xX) ‏نیاز به جملاتی در پایگاه دانش داریم که با‎ i. 557 ‏سيس يكسان ساز را به ( 01,36[ )112165 اعمال مى كنيم‎ Knows( John, x) = Hates( John ,x ) 

صفحه 13:
فصل هشتم: استتا در منطق مرتيه اول _ 76 و ۷ ‎Knows( John , Knows(y,‏ ‎We 0 0 9‏ 1 سس دده مسمس ممعم 1 و 7 به طور ضمنوهارلیس ور عمومی‌هستند Knows( John , JAY Knows( John, x) , Knows( John, Jane) ) Knows(y, eee 17۵1517520 Knows( John ,x) , Knows(y, Leonid) ) = {x/Leonid , y/John } 

صفحه 14:
فصل هشتم: استتا در منطق مرتيه اول _ 76 6 ۹ John ,x) , Knows(y, mother(y) ) ) {y/John , x/mother( John ) } ‎Knows(x ,‏ ‎Knows(x, Elizabeth ) )‏ 1232 1 < آخرین یکسان سازی با شکست مواجه می شود زیرا ا نمی تواند هم 0111[ باشد و هم ‏لل ۱۱۱۳/۰ از آنجايى كه 01112[از هر كسى ‎aS‏ ۱ ‏۱ ی = ا ‏20 را 

صفحه 15:
فصل هشتم: استتا در منطق مرتيه اول _ 76 یک راه مقابله با اين مشکل : ای کین رت ان ی ی ار رت ۱ UNIFY( Knows( John , x, ) , Knows(x,, Elizabeth ) ) ‎x, / Elizabeth , x, / John }‏ { ‎reper rae‏ ۱ بله, زیرا دو جمله زیر معنی مشابهی را می دهند : ‎Vx Knows(x, Elizabetir )‏ ‎Vx, Knows( x, , Elizabeth ) ‎ 

صفحه 16:
Lk 01 ee YS) Most General Unifier (Examples) P(e) ‏الماك‎ ۱ yey CGE ACO IG yen Cle) Mitueten ein P(P(&), v, BV) P(P(&), z, Ox) hv, xhy}or{y/z,zhs} ‎PO, vy, z) {®/x, Bly, B/}‏ (©© ,© ,مط ‎CD P(x, x) ORCL Oat‏ ‎@(u))‏ ‎P(x, P(x) Cae Ov OCO! 

صفحه 17:
Lk 01 ee YS) ۳۳ 0 به > و عقب ‎Ruan D Backward‏ - زنجيرهسازي به جلو (ع)ستستهطه له حده]): انم با جملات موجود در پایگاه دانش شروع کنیم و نتایج جديدي را که مي‌توانند ا ل لل ل ل ل ال ا ناميده مي شود. قانون 20126125 11001115 تعميم يافته به دو صورت استفاده مى شود. مى د این روش زماني استفاده مي‌شود که حقیقت جديدي به پایگاه داده ما اضافه شده باشد و خواسته باشیم نتایج آن را تولید کنیم. 

صفحه 18:
فصل هشتم: استتام در منطق مرتبه اول _ 76 ‎epee SE,‏ را ال اناا ‎[0 Wd en Sees Pep oem Pew Nee] ROE Cr soe PE oe ce) 00000 cs vom Terrie Up mee mPa ey er ees 21111010 eC ‏اين روش زماني استفاده ميشود كه هدفي براي اثبات وجود داشته باشد 

صفحه 19:
۱100 در منطق مرتيه اول ©3 ‎Completeness‏ ‏تصور کنید که ما پایگاه دانش زیر را در اختیار داریم: , 090 دمم 5300-00 ‎re ered‏ ا ا ا ا 6ه 5160-0 ل 000 يا ()2 يا (2)8 ددرست است. 

صفحه 20:
فصل هشتم: استناو در منطق ‎olay‏ 7 كا متأسفانه زنجيرهسازي با 20116138 1100115 نمىتواند (5)4 را نتيجه بكيرد ‎corey‏ ا وا ل الو ‎PRY CD Cin)‏ 0 ار | از اين رو توسط 120116115 1۷1001115 نمي‌تواند ‎ase‏ 3 اين بدان معنى است كه رويه اثباتى كه از 20116115 1100115 استفاده م ىكند ناكامل 25000 ار ۲ ۲ ‎ED os‏ ا ا ا ا 

صفحه 21:
01 ee YS) ‏يكروبيماستتنتاج‎ 1102 0 ال ا ا ۷ سس ‎er‏ ‏ل 8,۵ 10 سس ۳ ۰ | ‎tee Lee Re ee es ed]‏ ا ا 0 فصلى [] بايد درست باشدء از اين رو [] يا (] بايد درست باشد او ۱ انتيجه دومي 0-6 مي‌کند. 5 11001158 لجانه لستخرلج تركيبشرطىجديد را نمىدهد و فقط نتايج لتمىرا لمستخرلج مىكند از لمينرو قانون 1065111211010 قديتمندتر از ا نك 21 

صفحه 22:
۸ Auer eee anne YI :1650[10 ‏قانون استنتاج‎ [0 ICO Se Oran ‏ال‎ CSO Se) ‏ما مي‌توانيم این قانون را براي دو ترکیب فصلي به هر طولي وسعت بخشیم.‎ ‏که اگر يكي از قسمت‌هاي ترکیب فصلي در یک(:0181156)۳۴ با نقیض قسمت دیگر‎ ترکیب فصلي (,6) یکسان باشند. سپس ترکیب فصلي از تمام 3 ت‌ها استنتاج مي‌شود بغیر از آن دون ‎Resolution‏ تعميم‌یافته (ترکیباتف صلیع 0 تعميم يافته (تركيبات شرطى) ‎ 

صفحه 23:
فصل هشتم: استنتاو در منطق مرتبه اول ©3 ‎Resolution‏ تعميميافته(تركيبات ف صلیاي لیترالهای ,۳و 4 با فرض 4,0 کر (ظ) 11۳ داریم: 

صفحه 24:
aS [15 wa) ‎See) Resolution‏ كك رق ‎eee ie ee ear ercit‏ ا 0 ۵ ۱0۱۱۱ ‎ 

صفحه 25:
Ok Puereee eee ort) ‏فرمهاى كانونى‎ Pero ps eer gee ear earn | ee ‏ا ا‎ nee Soe ee tee edges CNF (Conjuction Normal Form) ‏فرمء فرم نرمال عطفى‎ فى فود در نسخه دوم قانون 11651112311012 . هر جمله يك تركيب شرطى شامل يك تركيب عطفى از اتمها در سمت جب و يك تركيب فصلى از اتمها در سمت راست است اين حالت. فرم نرمال شرطى 110170281 1102:11576م122) 1211 0 10) 0019) 

صفحه 26:
01 ee YS) قانون 1165011111012 تعميمى 5 ‎«aw! Modus Ponens‏ شرطى رايجتر از فرم 1101572 است. به دليل اينكه طرف سمت راست مى تواند يك ا ا 0 ۲ ‎tarps peg Sele Sor wa O pe eve‏ ا ا م ا مى توان ديد كه 20126125 21/100115 يك مورد ويزه از 1865111861013 است: Modus ponens : Resulation : ‎a=B Bae Mon‏ كنا ‎B True = 6 ‎Pre el pear ark a] ene] FS etre) Modus Ponens ‎Resear) Fst eri CEB AclsJo) ths (0) SRS AEE) ee ne Teeny a eer 

صفحه 27:
۳ ۳۹ Ok Puereee eee ort) ‏برهان خلف:‎ رويه استنتاج كاملى كه از 165011111012 استفاده مىكند برهان خلف (6111]23102© ناميده مىشود و همجنين به عنوان اثبات توسط تناقض ‎reduction and absurdum), proof by contradiction)‏ (KB ag) > Pc) = (KB Sq) ‏معتبر است ؟‎ [Pale ‏مثال: جمله‎ ا ل لت ل و م ا ا ا الل ‎rae Romer | ee aie‏ 

صفحه 28:
3© ‏در منطق مرتيه اول‎ ۱100 5)۸( ‏اثبات جمله‎ ‏الك سانا‎ . =P@)=R@&) . O@) = S@) R(z) Agi} ‏سس‎ =n P(w) = S(w)=P(x) = R(x) = P(x) * R(x) = ‏تین‎ 9 9 ‎arI¢4)‏ ۱ ۶ ۱ ‎True = S(x) S(A) = False‏ د ل ‎True >‏ ا اثباتى كه نشان مى دهد (5)4 از 3 استفاده از 36510160 با برهان خلف استنتاج مى شود 

صفحه 29:
aS [15 wa) Oe Rese Sl SD ee ene eed ‏از یک مجموعه از جملات به فرم نرمال مي‌توانيم اثبات کنیم که یک جمله‎ ا ل 

صفحه 30:
3 [151۳ 0 1 حذف ترکیب شرطي: ۰ ۲ 7 0 با 10 2 حذف نقیض : — 0 نقیض فقط براي فرم نرمال عطفي مجاز است. ‎se @ = =p‏ = 0 ee Dene yeas ten e) ‏مد 2 ود‎ a : ١ ۷-0 ‏نقیض را می توان با قوانین دمورگان حذف کرد‎ ‏سب‎ =p aVx p = 3x 1 

صفحه 31:
و 5 ۱1010 در منطق مرتيه اول ©3 3. استاندارد كردن متغيرها: ی فا را تا ی ار ار ‎eee ager‏ ۲ 0.4 1 ۷ وس ‎Vx P(x) Y Sx‏ 060 00 Vx dy P(x) 7 Rare Saree ene Slory Qy) 5 استفاده از تابع 51601070: بردازٍشئلستكه در لنتمام سورهاووجوديحذف مين وند (بسولساس‌قانونحذفسور وجودی ۲ ‎ax P(x)—— P(A)‏ Pe ‏ا‎ ale oe eR ee oer pee a) A oa 

صفحه 32:
3© ‏فصل هشتم: استنتاو در منطق مرتبه اول‎ "Every one has a heart“ a> ‏مثال:‎ ‎vx Person(x) = iy Heart(y) * (9, 10 Vx Person(x) => Heart(H) * Has(x,H) اگر بجای 16 اشخاص قرار گیرند آنوقت جمله بالا برای هر شخصی قلب مشابه 1 است نياز است بكوييم قلبى كه آنها دارند لزوماً بين آنها تقسيم نشده است!!!ا ۱ => Heart( F(x) ) * Has(x, F(x) ) 

صفحه 33:
Lk 01 ee YS) ‎KB pee or en oer pen ee F‏ ديدم نموشود ‎i=)‏ کی ناميدم موشود). ‏در حالت كلىء متغير سور وجودى توسط ترمى كه شامل تابع 512016112 باشد جايكزين مى شود. 516016112122:1012 تمام متغيرهاى سور وجودى را حذف ‏ی تن ‏بنابراین پس از آن. حذف سورهای عمومی مجاز می باشد 6 توزیع لا بر ۲: ‎(a‘c)(a‘c)‏ 9( 0 7. ساده سازى تركيبات: ‎ee (a*b’c)‏ ‎(a*b)‘c = (a*b‘c) 

صفحه 34:
LM ere ane ys) ‏تمرین؛‎ ‏رن‎ Se UID Dep EeN Ce 1- ‏]ع‎ 202 - 0060[ + 8)4( on a ‏لك‎ 2-0 Vx[S(x,A)= L@&,B)] => H(A) cos A.B 

07 Alireza yousefpouryousefpour@shomal.ac .ir  استنتاج در منطق مرتبه اول:فصل هشتم قوانین استنتاج منطق مرتبه اول 1. Modus 2. And – P Q, P Ponens ____________ Q 3. And – Introduction 1 ,2 , … ,n ____________  1 2  … n 5. Resolution  ,   __________   1 2  Elimination … n ______________  i 4. Or – i Introduction ____________  1 2  … n OR   ,   ____________     فصل هشتم :استنتاج در منطق مرتبه اول عالمت ) SUBST(,برای شرح نتیجه بکارگیری جانشینی در جمله  از عالمت ):SUBST(, استفاده می شود. = = ) )SUBST( {x/hamid} , male(x ) Male( hamid ) )SUBST( {x/Sam , y/Pam } , like(x,y ) like( Sam, Pam ترم زمینی :g ترمی بدون متغیر را گویند ‏Ali ) Missle ( M1 ) Father ( Hossein , Hamid فصل هشتم :استنتاج در منطق مرتبه اول سه قانون استنتاجي جديد: .1حذف سور عمومی ‏Universal Elimination برای هر جمله ، متغیر vو ترم زمینی gداریم: ‏ v,  ________________ ‏SUBST( {v/g} , )  )  x, Likes( x , icecream ________________________ ) SUBST( {x/BEN} , Likes( BEN , icecream ) استنباط جانشین فصل هشتم :استنتاج در منطق مرتبه اول .2حذف سور وجودی ‏Existential Elimination برای هر جمله ، متغیر Vو ثابت Kکه جای دیگر پایگاه دانش ظاهر نشده است داریم: ‏ v,  ________________ ‏SUBST( {v/K} , )  )  x, Kill( x , victim ________________________ ‏SUBST( {x/Murderer} , Kill( Murderer , ) ) victim استنباط جانشین فصل هشتم :استنتاج در منطق مرتبه اول .3معرفی سور وجودی ‏Existential Introduction برای هر جمله ، متغیر vکه در وجود ندارد و ترم زمینی gکه در موجود است داریم: ‏ ________________ ) v, SUBST( {g/v} ,  ) Likes ( jerry , icecream _____________________ ) x likes ( x , icecream } SUBST( { jerry/xبا جانشینی ) فصل هشتم :استنتاج در منطق مرتبه اول ‏Generelined Modus Ponens مودس پوننس تعمیم یافته ) (GMP تعمیمی از قانون استنتاج Modus Ponensکه شامل And- ،Introductionحذف سور عمومی و Modus ponensاست برای جمالت اتمی piو p’iو qکه برای تمامی iها آنگاه : ) SUBST(,p’i ) = SUBST(,piوجود دارد ‏p1 p2 …  pn  q ‏p’1 , p’2 , … , p’n __________________ )  SUBST( , q فصل هشتم :استنتاج در منطق مرتبه اول مثال: )Missile( M1 )Owns (NONO, M1 ‏x Missile(x)  owns( NONO , x)  sells( WEST , ) NONO, x در یک مرحله با جانشینی { }x/ M1جمله جدید زیر استنباط می شود: ‏sells( WEST , NONO, ) M1 یافتن xای در پایگاه دانش که چنین xای موشک است و NONOمالک xاست و سپس ثابت شود که WESTاین موشک را به NONOمی فروشد فصل هشتم :استنتاج در منطق مرتبه اول Modus Ponensبه سه دلیل یک قانون استنتاج موثر است : با ترکیب تعدادی از استنتاج های کوچک و تبدیل آن به یک استنتاج بزرگ مراحل زیادی را تقلیل می دهد این قانون از جانشینی هایی استفاده می کند که موثر بودنشان (برعکس حذف تصادفی سور عمومی) ضمانت می شود .الگوریتم یکسان سازی دو جمله را می گیرد و جانشینی ا در صورت وجود برمیگرداند که آن دو جمله یکسان شوند این قانون تمام جمالت موجود در پایگاه دانش را به فرم کانونی در می آورد .انجام این عمل یکبار در مرحله آغازین ،ما را از اتالف زمان برای انجام تبدیالت در طول مرحله اثبات بی نیاز می کند فصل هشتم :استنتاج در منطق مرتبه اول ‏Canonic فرم کانونی alاستنتاج مودس پوننس تعمیم یافته ()GMP سعی می کنیم تا مکانیزیم استنتاجی را با قانون بوجود آوریم .تمام جمالت موجود در پایگاه دانش باید بصورتی باشند که با یکی از فرضیات قانون GMPمطابقت داشته باشند. فرم کانونی برای GMPمتضمن این نکته است که هر جمله در پايگاه دانش باید از نوع اتمي يا شرطي (با يک ترکيب عطفي از جمالت اتمي در طرف چپ و يک اتم منفرد در طرف راست ) باشد. جمالتی از این قبیل جمالت هورن ( )Horn sentenceنامیده می شود پایگاه دانشی که فقط شامل جمالت هورن باشد Horn Normal Formنامیده می شود ما جمالت را به جمالت Hornزماني تبديل مي‌کنيم که ابتدا وارد پايگاه دانش ،با استفاده از حذف سور وجودي و حذف Andشده باشند مثال: ) x Owns( Nono, x )  Missile( x به دو جمله اتمی هورن شامل ) Owns( Nono , M1و ) Missile( M1تبدیل می شود فصل هشتم :استنتاج در منطق مرتبه اول یکسان سازی Unificatio جانشینی را در صورت وجود برمیگرداند ت[[ا الگوریتم یکسان سازی دو جمله را می گیرد وn آن دو جمله یکسان شوند وظيفه روتين يکسان‌ساز ،Unifyگرفتن دو جمله اتمي p، qو برگرداندن يک جانشين که p، qرا مشابه هم خواهد ساخت( .،اگ[[ر چ[[نين جانش[[يني موج[[ود نباش[[دUnify، ، failبرمي‌گرداند). = )( SUBST(,p ‏ ‏UNIFY( p , q ) =  ) ) SUBST( ,q جانشین – یکسان ساز ،UNIFYعم[[[[ومي‌ترين يکسان‌س[[[[از ( )Most General Unifierيا ( )MGUرا برمي‌گرداند ،که جانشيني است که کمترين تعهد را در قبل محدودس[[ازي متغيرها دارد. فصل هشتم :استنتاج در منطق مرتبه اول مثال :دانش کسب شده “ “ John hates everyone he knows می خواهیم با استفاده از قانون استنتاج مودس پوننس کشف کنیم که Johnاز چه کسی متنفر است یعنی: باشد. نیاز به جمالتی در پایگاه دانش داریم که با ) Knows( John, xیکسان سپس یکسان ساز را به ) Hates( John, xاعمال می کنیم. ) Knows( John, x )  Hates( John ,x  استنتاج در منطق مرتبه اول:فصل هشتم KB Knows( John , Jane ) Knows( y , mother(y) ) فرض کنید پایگاه دانش شامل جمالت زیر باشد Knows( y , Leonid ) Knows( x , Elizabeth ) به طور ضمنی دارای سور عمومی هستندy وx Knows( John , Jane ) Knows( John , x ) , Knows( John , Jane ) ) UNIFY( = {x/ Knows( y, Jane } UNIFY( )Knows( John , x ) , Knows( y , Leonid ) ) = Leonid { x / Leonid , y / John } فصل هشتم :استنتاج در منطق مرتبه اول ‏Knows( y , )mother(y ) (UNIFY( Knows ) ) )John , x ) , Knows( y , mother(y = { y / John , x / (Knows }) x, ‏mother( John ‏Elizabeth ) (UNIFY (Knows ) ) John , x ) , Knows( x , Elizabeth آخرین یکسان سازی با شکست مواجه می شود زیرا xنمی تواند هم Johnباشد و هم ‏Elizabeth از آنجایی که Johnاز هر کسی که مشناسد متنفر است و نیز همه Elizabethرا می شناسند = Fail پس باید قادر باشیم استنباط کنیم که Johnاز Elizabethمتنفر است فصل هشتم :استنتاج در منطق مرتبه اول یک راه مقابله با این مشکل : استاندارد کردن متغیرها در دو جمله یکسان است یعنی که اسامی متغیرها را تغییر دهیم تا از تشابه دو نام جلوگیری کرده باشیم ) ) UNIFY( Knows( John , x1 ) , Knows( x2 , Elizabeth = { x1 / Elizabeth , x2 / } John آیا تغییر نام معتبر است ؟ بله ،زیرا دو جمله زیر معنی مشابهی را می دهند ) x Knows( x , Elizabeth ) x2 Knows( x2 , Elizabeth  استنتاج در منطق مرتبه اول:فصل هشتم Most General Unifier (Examples) w1 P(x) P(F(x), y, G(x)) P(F(x), y, G(y)) P(x, B, B) P(G(F(v)), G(u)) P(x, F(x)) w2 MGU P(A) P(F(x), x, G(x)) P(F(x), z, G(x)) P(A, y, z) P(x, x) {A/x} {y/x} or {x/y} {z/y, x/y}or{y/z,z/x} {A/x, B/y, B/z} {F(v)/u, G(u)/x} P(x, x) No MGU! فصل هشتم :استنتاج در منطق مرتبه اول زنجيره‌سازي به جلو و عقب (Forward AND Backward )Chaining زنجيره‌سازي به جلو (:)forward chainingقانون Modus Ponensتعميم يافته به دو صورت استفاده مي‌شود .مي‌ت[[وانيم با جمالت موجود در پايگاه دانش شروع کنيم و نت[[ايج جديدي را ک[[ه مي‌توانن[[د استنباط‌هاي بيشتري را بس[[ازند ،توليد ک[[نيم .اين روش زنجيره‌س[[ازي ب[[ه جل[[و ناميده مي‌شود. اين روش زماني استفاده مي‌شود که حقيقت جديدي به پايگ[[اه داده م[[ا اض[[افه ش[[ده باشد و خواسته باشيم نتايج آن را توليد کنيم. فصل هشتم :استنتاج در منطق مرتبه اول -2زنجيره‌سازي به عقب (:)Backward Chaining مي‌توانيم با چيزي که قصد اثباتش را داريم آغاز کنيم و جمالت ش[[رطي را پيدا ک[[نيم ک[ه ب[ه م[ا اج[ازه بدهن[د نتيج[ه را از آنه[ا اس[تنتاج ک[نيم ،و س[پس س[عي در ايج[اد پيش‌فرضيات آنها داشته باشيم. اين روش زماني استفاده مي‌شود که هدفي براي اثبات وجود داشته باشد. فصل هشتم :استنتاج در منطق مرتبه اول کامل بودن Completeness : تصور کنيد که ما پايگاه دانش زير را در اختيار داريم: )P(x)  Q(x )P(x)  R(x سپس ما مي‌خواهيم که ) S(Aرا نتيجه بگيريمQ(x)  S(x) ، )R(x)  S(x ‏KB ‏x ‏x ‏x ‏x )Q(Aيا ) R(Aدرست باشد ،و يکي از آنها بايد درست باشد زيرا: ‌ ) S(Aدرست است ،اگر يا ) P(Aيا ) ¬ P(Aدرست است. فصل هشتم :استنتاج در منطق مرتبه اول يتوان[[د ) S(Aرا متأسفانه ،زنجيره‌سازي ب[[ا Modus Ponensنم ‌ نتيجه بگيرد. مشکل اين است که ) x P(x)  R(xنمي‌تواند به صورت Hornدربيايد ،و از اين رو توسط Modus Ponensنمي‌تواند استفاده شود. اين بدان معني است که رويه اثب[[اتي ک[[ه از Modus Ponensاس[[تفاده مي‌کن[[د ناکامل ( )incompleteاست: جمالتي که در پايگاه دانش مستلزم شده‌اند که رويه نمي‌تواند آنها را استنتاج کند. فصل هشتم :استنتاج در منطق مرتبه اول :Resolutionيک رويه استنتاج کامل صورت ساده قانون استنتاج Resulationبرای منطق گزاره ای به فرم زیر است: ‏  ,   ______________ ‏    ‏ ,   ____________ ‏OR ‏  قانون به دو روش درک می شود. اگر نادرست باشد ،در اولین ترکیب فصلی باید درست باشد پس از دومین ترکیب فصلی باید درست باشد ،از این رو یا باید درست باشد از دو ترکيب شرطي مي‌توانيم ترکيب سومي را مشتق ک[[نيم ک[[ه پيش‌ف[[رض اولي را ب[[ه نتيجه دومي متصل مي‌کند. Modus Ponensاجازه استخراج ترکیب شرطی جدید را نمی دهد و فقط نت[[ایج اتمی را استخراج می کند از اینرو قانون Resulationقدرتمندتر از Modus Ponensاست فصل هشتم :استنتاج در منطق مرتبه اول قانون استنتاج :resolution در فرم ساده قانون ،resolutionپيش‌فرضيات داراي دقيقًا دو ترکيب فصلي هس[[تند. ما مي‌توانيم اين قانون را براي دو ترکيب فصلي به هر طولي وسعت بخشيم، که اگر يکي از قسمت‌هاي ترکيب فصلي در يک) clause(Pjب[[ا نقيض قس[[مت ديگ[[ر ترکيب فصلي ( )qkيکسان باشند ،سپس ترکيب فصلي از تمام قسمت‌ها استنتاج مي‌ش[[ود بغير از آن دو: Resolutionتعميم يافته (ترکيبات فصلي) Resolution تعميم يافته (ترکيبات شرطي) فصل هشتم :استنتاج در منطق مرتبه اول Resolutionتعميم يافته (ترکيبات فصلي): ‌ براي لیترالهای Piو qiبا فرض UNIFY (Pj ,¬ qk)=θداریم: ‏Pm ‏qn ...  ... Pj ‏ ...  ... qk ‏ ‏P1 ‏q1 ‏SUBST )) ( ,(P1  ...Pj 1  Pj1 ...pm  q1  ...qk 1  qk1 ...qn  استنتاج در منطق مرتبه اول:فصل هشتم :) تعميم يافته (ترکيبات شرطيResolution UNIFY (Pj , qk)=θ کهsi وri وqi وPi براي اتم‌هاي P1  s1  ... ... Pj ...  sn3  q1  Pn1  r1  ... rn2 ... qk ... qn4 SUBST ( ,(P1  ...Pj 1  Pj1  pn1  s1  ...sn3  r1  ...rn2  q1  ...qk 1  qk1  ... qn4)) فصل هشتم :استنتاج در منطق مرتبه اول فرمهای کانونی ‏Resulation ، Resulationهر جمله یک ترکیب فصلی است .تمام در نسخه اولیه قانون ترکیبات فصلی در KBبه صورت ترکیب عطفی به هم وصل شده اند بنابراین این فرم ،فرم نرمال عطفی ) CNF (Conjuction Normal Formنامیده می شود. در نسخه دوم قانون ، Resulationهر جمله یک ترکیب شرطی شامل یک ترکیب عطفی از اتمها در سمت چپ و یک ترکیب فصلی از اتمها در سمت راست است این حالت ،فرم نرمال شرطی INF (Implicative Normal ) Formنامیده می شود. فصل هشتم :استنتاج در منطق مرتبه اول قانون Resolutionتعميمي از Modus Ponensاست. شرطي رايج‌تر از فرم Hornاست ،به دليل اينکه طرف سمت راست مي‌تواند يک ترکيب شرطي باشد و نه فقط يک اتم تنها. جمله اتمی به فرم نرمال شرطی به صورت True  نوشته می شود، می توان دید که Modus Ponensیک مورد ویژه از Resulationاست: ‏Resulation : ‏True  ,  _________________ ‏True   ‏Modus ponens : ‏a ,  ___________ ‏ Modus Ponensقابليت ت@@رکيب اتم‌ه@@ا ب@@ا يک ت@@رکيب ش@@رطي را ب@@ه منظ@@ور استخراج نتيجه به صورتي دارد که resolutionقادر به انجام آن نيست. فصل هشتم :استنتاج در منطق مرتبه اول برهان خلف: رويه اس[[[تنتاج ک[[[املي ک[[[ه از resolutionاس[[[تفاده مي‌کن[[[د بره[[[ان خل[[[ف ( )refutationناميده مي‌شود و هم‌چنين به عنوان اثبات توسط تناقض ( )proof by contradictionو (reduction and absurdum شناخته شده است. ) ( KB  q ‏ ) ( KB  q )  False مثال :جمله PPمعتبر است ؟ ابتدا فرض می کنیم جمله اول نادرست است (برهان خلف) نادرست( P  P ) = P  (P) = P  یک جمله همیشه P پس جمله اول درست است  استنتاج در منطق مرتبه اول:فصل هشتم P(w)  Q(w) ,  S(z) {z/w} S(A) اثبات جمله P(x)  R(x) , Q(z)  S(z) , R(z) P(w)  S(w) P(x)  R(x) = P(x)  R(x) = True  P(x)  R(x) {w/x} True  S(x)  R(x) {x/z} R(z)  S(z) True  S(x) S(A)  False {x/A} True  False باResulation با استفاده ازKB ازS(A) اثباتی که نشان می دهد برهان خلف استنتاج می شود فصل هشتم :استنتاج در منطق مرتبه اول تبديل به فرم نرمال: هر جمله مرتبه اولي مي‌تواند به صورت فرم نرمال شرطي (يا عطفي) دربيايد. از يک مجموعه از جمالت به فرم نرمال مي‌توانيم اثبات کنيم که يک جمل[[ه نرمال از مجموعه پيروي خواهد کرد. فصل هشتم :استنتاج در منطق مرتبه اول الگوریتم تبديل به فرم نرمال: .1حذف ترکيب شرطي: p  qبا pq .2حذف نقیض : نقيض فقط براي فرم نرمال عطفي مجاز است، و براي تمام فرم‌هاي نرمال شرطي ممنوع است. نقیض را می توان با قوانین دمورگان حذف کرد ‏ p ‏ p ‏ p ‏ x )(pq ‏q )(pq ‏q ‏p ‏x p ‏p فصل هشتم :استنتاج در منطق مرتبه اول .3استاندارد کردن متغيرها: جمالتی که از متغیرهای مشابه استفاده می کنند تغییر نام می دهیم ت[[ا از ابهام[[ات در زمان حذف سورها جلوگیری شود ‏x P(x)  x )Q(x ‏x P(x)  y )Q(y .4انتقال سورها به سمت چپ ‏P(x)  ‏x y )Q(y .5استفاده از تابع :Skolem Skolemizationپردازش[[ي اس[[ت ک[[ه در آن تم[[ام س[[ورهاي وج[[ودي ح[[ذف مي‌شوند( .براساس قانون حذف سور وجودی) )P(A )P(x ‏x Aثابتی است که در هیچ جای پایگاه داده دیده نمی شود فصل هشتم :استنتاج در منطق مرتبه اول مثال :جمله “”Every one has a heart ‏y Heart(y)  اگر فقط yرا با Hجایگزین کنیم داریم ‏x Person(x)  )Has(x,y ‏x Person(x)  Heart(H)  )Has(x,H اگر بجای xاشخاص قرار گیرند آنوقت جمله باال برای هر شخصی قلب مشابه Hاست نیاز است بگوییم قلبی که آنها دارند لزومٌا بین آنها تقسیم نشده است!!! ‏x Person(x)  Heart( F(x) )  ) )Has(x, F(x فصل هشتم :استنتاج در منطق مرتبه اول Fنام تابعی است که جای دیگری از KBدیده نمی شود ( Fیک تابع Skolemنامیده می شود). در حالت کلی ،متغیر سور وجودی توسط ترمی که شامل تابع Skolemباشد جایگزین می شود Skolemization .تمام متغیرهای سور وجودی را حذف می کند. بنابراین پس از آن ،حذف سورهای عمومی مجاز می باشد .6توزیع بر :  .7ساده سازی ترکیبات : )( ab)c = (ac)(ac )( ab)c = (abc )( ab)c = (abc فصل هشتم :استنتاج در منطق مرتبه اول تمرین: جمالت زیر را به فرم CNFتبدیل نمایید. ثابت x [ P(x)  Q(x) ]  R(A) , 1- ثابت x [ S(x,A)  L(x,B) ]  H(A) , 2A,B ‏A