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

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

اسلاید 1: 07فصل نهماستنتاج در منطق مرتبه اولAlireza yousefpouryousefpour@shomal.ac.ir

اسلاید 2: قوانین استنتاج منطق مرتبه اولفصل هشتم: استنتاج در منطق مرتبه اول1. Modus Ponens2. And – Elimination3. And – Introduction4. Or – Introduction5. Resolution P  Q , P ____________ Q 1 2  … n______________ i 1 ,2 , … ,n____________ 1 2  … n ,  __________   ,  ____________   ORi____________ 1 2  … n

اسلاید 3: علامت SUBST(,):از علامت SUBST(,) برای شرح نتیجه بکارگیری جانشینی  در جمله  استفاده می شود. SUBST( {x/hamid} , male(x) ) = Male( hamid )SUBST( {x/Sam , y/Pam } , like(x,y) ) = like( Sam, Pam )ترم زمینی g:ترمی بدون متغیر را گویندMissle ( M1 )AliFather ( Hossein , Hamid )فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 4: 1. حذف سور عمومی سه قانون استنتاجي جديد:Universal Eliminationبرای هر جمله  ، متغیر v و ترم زمینی g داریم: v, ________________SUBST( {v/g} ,  ) x, Likes( x , icecream )________________________SUBST( {x/BEN} , Likes( BEN , icecream ) )جانشیناستنباطفصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 5: 2. حذف سور وجودیExistential Elimination v, ________________SUBST( {v/K} ,  )جانشیناستنباطبرای هر جمله  ، متغیر V و ثابت K که جای دیگر پایگاه دانش ظاهر نشده است داریم: x, Kill( x , victim )________________________SUBST( {x/Murderer} , Kill( Murderer , victim ) )فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 6: برای هر جمله  ، متغیر v که در  وجود ندارد و ترم زمینی g که در  موجود است داریم:________________v, SUBST( {g/v} ,  )Likes ( jerry , icecream )_____________________x likes ( x , icecream )با جانشینیSUBST( { jerry/x} )3. معرفی سور وجودیExistential Introductionفصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 7: مودس پوننس تعمیم یافته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 )فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 8: مثال: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 می فروشدفصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 9: Modus Ponens به سه دلیل یک قانون استنتاج موثر است : با ترکیب تعدادی از استنتاج های کوچک و تبدیل آن به یک استنتاج بزرگ مراحل زیادی را تقلیل می دهد این قانون از جانشینی هایی استفاده می کند که موثر بودنشان (برعکس حذف تصادفی سور عمومی) ضمانت می شود. الگوریتم یکسان سازی دو جمله را می گیرد و جانشینی ا در صورت وجود برمیگرداند که آن دو جمله یکسان شوند این قانون تمام جملات موجود در پایگاه دانش را به فرم کانونی در می آورد. انجام این عمل یکبار در مرحله آغازین، ما را از اتلاف زمان برای انجام تبدیلات در طول مرحله اثبات بی نیاز می کندفصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 10: فرم کانونیCanonicalسعی می کنیم تا مکانیزیم استنتاجی را با قانون استنتاج مودس پوننس تعمیم یافته (GMP) بوجود آوریم. تمام جملات موجود در پایگاه دانش باید بصورتی باشند که با یکی از فرضیات قانون GMP مطابقت داشته باشند.فرم کانونی برای GMP متضمن این نکته است که هر جمله در پايگاه دانش باید از نوع اتمي يا شرطي (با يک ترکيب عطفي از جملات اتمي در طرف چپ و يک اتم منفرد در طرف راست ) باشد.جملاتی از این قبیل جملات هورن (Horn sentence) نامیده می شودپایگاه دانشی که فقط شامل جملات هورن باشد Horn Normal Form نامیده می شودما جملات را به جملات Horn زماني تبديل مي‌کنيم که ابتدا وارد پايگاه دانش، با استفاده از حذف سور وجودي و حذف And شده باشندمثال:x Owns( Nono, x )  Missile( x )به دو جمله اتمی هورن شامل Owns( Nono , M1 ) و Missile( M1 ) تبدیل می شودفصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 11: یکسان سازی Unificationالگوریتم یکسان سازی دو جمله را می گیرد و جانشینی را در صورت وجود برمیگرداند تا آن دو جمله یکسان شوندوظيفه روتين يکسان‌ساز Unify، گرفتن دو جمله اتمي p، q و برگرداندن يک جانشين که p، q را مشابه هم خواهد ساخت،. (اگر چنين جانشيني موجود نباشد، Unify، fail برمي‌گرداند.)UNIFY، عمومي‌ترين يکسان‌ساز (Most General Unifier) يا (MGU) را برمي‌گرداند، که جانشيني است که کمترين تعهد را در قبل محدودسازي متغيرها دارد.UNIFY( p , q ) =   ( SUBST(,p) = SUBST( ,q ) )جانشین – یکسان سازفصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 12: مثال:دانش کسب شده“ John hates everyone he knows “می خواهیم با استفاده از قانون استنتاج مودس پوننس کشف کنیم که John از چه کسی متنفر است یعنی: نیاز به جملاتی در پایگاه دانش داریم که با Knows( John, x) یکسان باشد. سپس یکسان ساز را به Hates( John, x ) اعمال می کنیم.Knows( John, x )  Hates( John ,x )فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 13: فرض کنید پایگاه دانش شامل جملات زیر باشدKnows( John , Jane )Knows( y , Leonid )Knows( y , mother(y) )Knows( x , Elizabeth )x و y به طور ضمنی دارای سور عمومی هستند Knows( John , Jane )UNIFY( Knows( John , x ) , Knows( John , Jane ) ) = { x / Jane }Knows( y , Leonid )UNIFY( Knows( John , x ) , Knows( y , Leonid ) ) = { x / Leonid , y / John }KBفصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 14: Knows( y , mother(y) )UNIFY( Knows( John , x ) , Knows( y , mother(y) ) ) = { y / John , x / mother( John ) }Knows( x , Elizabeth )UNIFY( Knows( John , x ) , Knows( x , Elizabeth ) ) = Failآخرین یکسان سازی با شکست مواجه می شود زیرا x نمی تواند هم John باشد و هم Elizabethاز آنجایی که John از هر کسی که مشناسد متنفر استو نیز همه Elizabeth را می شناسندپس باید قادر باشیم استنباط کنیم که John از Elizabeth متنفر استفصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 15: استاندارد کردن متغیرها در دو جمله یکسان است یعنی که اسامی متغیرها را تغییر دهیم تا از تشابه دو نام جلوگیری کرده باشیمUNIFY( Knows( John , x1 ) , Knows( x2 , Elizabeth ) ) = { x1 / Elizabeth , x2 / John }آیا تغییر نام معتبر است ؟بله، زیرا دو جمله زیر معنی مشابهی را می دهندx Knows( x , Elizabeth ) x2 Knows( x2 , Elizabeth ) یک راه مقابله با این مشکل :فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 16: فصل هشتم: استنتاج در منطق مرتبه اولMost General Unifier (Examples)

اسلاید 17: اين روش زماني استفاده مي‌شود که حقيقت جديدي به پايگاه داده ما اضافه شده باشد و خواسته باشيم نتايج آن را توليد کنيم.زنجيره‌سازي به جلو و عقب(Forward AND Backward Chaining)1- زنجيره‌سازي به جلو (forward chaining):قانون Modus Ponens تعميم يافته به دو صورت استفاده مي‌شود. مي‌توانيم با جملات موجود در پايگاه دانش شروع کنيم و نتايج جديدي را که مي‌توانند استنباط‌هاي بيشتري را بسازند، توليد کنيم. اين روش زنجيره‌سازي به جلو ناميده مي‌شود.فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 18: مي‌توانيم با چيزي که قصد اثباتش را داريم آغاز کنيم و جملات شرطي را پيدا کنيم که به ما اجازه بدهند نتيجه را از آنها استنتاج کنيم، و سپس سعي در ايجاد پيش‌فرضيات آنها داشته باشيم.اين روش زماني استفاده مي‌شود که هدفي براي اثبات وجود داشته باشد.2- زنجيره‌سازي به عقب (Backward Chaining):فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 19: S(A) درست است، اگر Q(A)‌يا R(A) درست باشد، و يکي از آنها بايد درست باشد زيرا: يا P(A) يا P(A) ¬ درست است.کامل بودن :Completenessتصور کنيد که ما پايگاه دانش زير را در اختيار داريم:x P(x)  Q(x)x P(x)  R(x)x Q(x)  S(x)x R(x)  S(x)KBسپس ما مي‌خواهيم که S(A) را نتيجه بگيريم،فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 20: مشکل اين است که x P(x)  R(x) نمي‌تواند به صورت Horn دربيايد، و از اين رو توسط Modus Ponens نمي‌تواند استفاده شود.اين بدان معني است که رويه اثباتي که از Modus Ponens استفاده مي‌کند ناکامل (incomplete) است: متأسفانه، زنجيره‌سازي با Modus Ponens نمي‌تواند S(A) را نتيجه بگيرد.جملاتي که در پايگاه دانش مستلزم شده‌اند که رويه نمي‌تواند آنها را استنتاج کند.فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 21: Resolution: يک رويه استنتاج کاملصورت ساده قانون استنتاج Resulation برای منطق گزاره ای به فرم زیر است:از دو ترکيب شرطي مي‌توانيم ترکيب سومي را مشتق کنيم که پيش‌فرض اولي را به نتيجه دومي متصل مي‌کند. ,  ____________   ,  ______________   ORقانون به دو روش درک می شود.اگر  نادرست باشد، در اولین ترکیب فصلی  باید درست باشد پس از دومین ترکیب فصلی  باید درست باشد، از این رو  یا  باید درست باشدModus Ponens اجازه استخراج ترکیب شرطی جدید را نمی دهد و فقط نتایج اتمی را استخراج می کند از اینرو قانون Resulation قدرتمندتر از Modus Ponens استفصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 22: در فرم ساده قانون resolution، پيش‌فرضيات داراي دقيقاً دو ترکيب فصلي هستند. ما مي‌توانيم اين قانون را براي دو ترکيب فصلي به هر طولي وسعت بخشيم، که اگر يکي از قسمت‌هاي ترکيب فصلي در يکclause(Pj) با نقيض قسمت ديگر ترکيب فصلي (qk) يکسان باشند، سپس ترکيب فصلي از تمام قسمت‌ها استنتاج مي‌شود بغير از آن دو:Resolution تعميم يافته (ترکيبات فصلي) Resolution تعميم يافته (ترکيبات شرطي)قانون استنتاج resolution:فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 23: براي لیترالهای Pi و qi با فرض UNIFY (Pj ,¬ qk)=θ داریم:Resolution‌ تعميم يافته (ترکيبات فصلي):فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 24: براي اتم‌هاي Pi و qi و ri و si که UNIFY (Pj , qk)=θResolution تعميم يافته (ترکيبات شرطي):فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 25: فرمهای کانونی Resulationدر نسخه اولیه قانون Resulation ، هر جمله یک ترکیب فصلی است. تمام ترکیبات فصلی در KB به صورت ترکیب عطفی به هم وصل شده اند بنابراین این فرم، فرم نرمال عطفی CNF (Conjuction Normal Form) نامیده می شود.در نسخه دوم قانون Resulation ، هر جمله یک ترکیب شرطی شامل یک ترکیب عطفی از اتمها در سمت چپ و یک ترکیب فصلی از اتمها در سمت راست است این حالت، فرم نرمال شرطی INF (Implicative Normal Form) نامیده می شود.فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 26: Modus Ponens قابليت ترکيب اتم‌ها با يک ترکيب شرطي را به منظور استخراج نتيجه به صورتي دارد که resolution قادر به انجام آن نيست.قانون Resolution تعميمي از Modus Ponens است.شرطي رايج‌تر از فرم Horn است، به دليل اينکه طرف سمت راست مي‌تواند يک ترکيب شرطي باشد و نه فقط يک اتم تنها.جمله اتمی  به فرم نرمال شرطی به صورت True   نوشته می شود،می توان دید که Modus Ponens یک مورد ویژه از Resulation است:Modus ponens : Resulation : , ___________ True  , _________________ True  فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 27: رويه استنتاج کاملي که از resolution استفاده مي‌کند برهان خلف (refutation) ناميده مي‌شود و هم‌چنين به عنوان اثبات توسط تناقض (proof by contradiction) و (reduction and absurdum شناخته شده است.برهان خلف:( KB  q )  False )  ( KB  q )مثال: جمله PP معتبر است ؟ابتدا فرض می کنیم جمله اول نادرست است (برهان خلف)( P  P ) = P  (P) = P  Pیک جمله همیشه نادرست پس جمله اول درست استفصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 28: اثبات جمله S(A)P(w)  Q(w) , P(x)  R(x) , Q(z)  S(z) , R(z)  S(z)P(w)  S(w) P(x)  R(x) = P(x)  R(x) = True  P(x)  R(x) True  S(x)  R(x) R(z)  S(z)True  S(x) S(A)  FalseTrue  Falseاثباتی که نشان می دهد S(A) از KB با استفاده از Resulation با برهان خلف استنتاج می شود{z/w}{w/x}{x/z}{x/A}فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 29: هر جمله مرتبه اولي مي‌تواند به صورت فرم نرمال شرطي (يا عطفي) دربيايد. از يک مجموعه از جملات به فرم نرمال مي‌توانيم اثبات کنيم که يک جمله نرمال از مجموعه پيروي خواهد کرد.تبديل به فرم نرمال:فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 30: الگوریتم تبديل به فرم نرمال:1. حذف ترکيب شرطي: p  q با pqنقيض فقط براي فرم نرمال عطفي مجاز است، و براي تمام فرم‌هاي نرمال شرطي ممنوع است.نقیض را می توان با قوانین دمورگان حذف کرد(pq)  p q(pq)  p qp  px p  x px p  xp2. حذف نقیض :فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 31: جملاتی که از متغیرهای مشابه استفاده می کنند تغییر نام می دهیم تا از ابهامات در زمان حذف سورها جلوگیری شودx P(x)  x Q(x)x P(x)  y Q(y)4. انتقال سورها به سمت چپx y P(x)  Q(y)Skolemization پردازشي است که در آن تمام سورهاي وجودي حذف مي‌شوند. (براساس قانون حذف سور وجودی)x P(x) P(A) A ثابتی است که در هیچ جای پایگاه داده دیده نمی شود3. استاندارد کردن متغيرها: 5. استفاده از تابع Skolem:فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 32: مثال:جمله “Every one has a heart”x Person(x)  y Heart(y)  Has(x,y)اگر فقط y را با H جایگزین کنیم داریمx Person(x)  Heart(H)  Has(x,H)اگر بجای x اشخاص قرار گیرند آنوقت جمله بالا برای هر شخصی قلب مشابه H استنیاز است بگوییم قلبی که آنها دارند لزوماٌ بین آنها تقسیم نشده است!!!x Person(x)  Heart( F(x) )  Has(x, F(x) )فصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 33: 6. توزیع  بر  :( ab)c = (ac)(ac)7. ساده سازی ترکیبات :( ab)c = (abc)( ab)c = (abc)F نام تابعی است که جای دیگری از KB دیده نمی شود (F یک تابع Skolem نامیده می شود).در حالت کلی، متغیر سور وجودی توسط ترمی که شامل تابع Skolem باشد جایگزین می شود. Skolemization تمام متغیرهای سور وجودی را حذف می کند. بنابراین پس از آن، حذف سورهای عمومی مجاز می باشدفصل هشتم: استنتاج در منطق مرتبه اول

اسلاید 34: جملات زیر را به فرم CNF تبدیل نمایید.1- x [ P(x)  Q(x) ]  R(A) , ثابت A2- x [ S(x,A)  L(x,B) ]  H(A) , ثابت A,Bتمرین:فصل هشتم: استنتاج در منطق مرتبه اول