بخشی از پاورپوینت
--- پاورپوینت شامل تصاویر میباشد ----
اسلاید 1 :
قوانين استنتاج منطق مرتبه اول
اسلاید 2 :
علامت SUBST(q,a):
از علامت SUBST(q,a) براي شرح نتيجه بکارگيري جانشيني q در جمله a استفاده مي شود.
ترم زميني g:
ترمي بدون متغير را گويند
اسلاید 3 :
سه قانون استنتاجي جديد:
حذف سور عمومي
براي هر جمله a ، متغير v و ترم زميني g داريم:
اسلاید 4 :
حذف سور وجودي
براي هر جمله a ، متغير V و ثابت K که جاي ديگر پايگاه دانش ظاهر نشده است داريم:
اسلاید 5 :
معرفي سور وجودي
براي هر جمله a ، متغير v که در a وجود ندارد و ترم زميني g که در a موجود است داريم:
اسلاید 6 :
مودس پوننس تعميم يافته
تعميمي از قانون استنتاج Modus Ponens که شامل And-Introduction، حذف سور عمومي و Modus ponens است
براي جملات اتمي pi و p’i و q که براي تمامي iها
SUBST(q,p’i ) = SUBST(q,pi) وجود دارد آنگاه :
اسلاید 7 :
Missile( M1)
Owns (NONO, M1)
"x Missile(x) Ù owns( NONO , x) Þ sells( WEST , NONO, x )
در يک مرحله با جانشيني {x/ M1} جمله جديد زير استنباط مي شود:
يافتن xاي در پايگاه دانش که چنين xاي موشک است و NONO مالک x است و سپس ثابت شود که WEST اين موشک را به NONO مي فروشد
اسلاید 8 :
Modus Ponens به سه دليل يک قانون استنتاج موثر است :
q با ترکيب تعدادي از استنتاج هاي کوچک و تبديل آن به يک استنتاج بزرگ مراحل زيادي را تقليل مي دهد
q اين قانون از جانشيني هايي استفاده مي کند که موثر بودنشان (برعکس حذف تصادفي سور عمومي) ضمانت مي شود. الگوريتم يکسان سازي دو جمله را مي گيرد و جانشيني ا در صورت وجود برميگرداند که آن دو جمله يکسان شوند
q اين قانون تمام جملات موجود در پايگاه دانش را به فرم کانوني در مي آورد. انجام اين عمل يکبار در مرحله آغازين، ما را از اتلاف زمان براي انجام تبديلات در طول مرحله اثبات بي نياز مي کند
اسلاید 9 :
فرم کانوني
سعي مي کنيم تا مکانيزيم استنتاجي را با قانون استنتاج مودس پوننس تعميم يافته (GMP) بوجود آوريم. تمام جملات موجود در پايگاه دانش بايد بصورتي باشند که با يکي از فرضيات قانون GMP مطابقت داشته باشند.
فرم کانوني براي GMP متضمن اين نکته است که هر جمله در پايگاه دانش بايد از نوع اتمي يا شرطي (با يک ترکيب عطفي از جملات اتمي در طرف چپ و يک اتم منفرد در طرف راست ) باشد.
جملاتي از اين قبيل جملات هورن (Horn sentence) ناميده مي شود
پايگاه دانشي که فقط شامل جملات هورن باشد Horn Normal Form ناميده مي شود
ما جملات را به جملات Horn زماني تبديل ميکنيم که ابتدا وارد پايگاه دانش، با استفاده از حذف سور وجودي و حذف And شده باشند
مثال:
به دو جمله اتمي هورن شامل Owns( Nono , M1 ) و Missile( M1 ) تبديل مي شود
اسلاید 10 :
يکسان سازي
الگوريتم يکسان سازي دو جمله را مي گيرد و جانشيني را در صورت وجود برميگرداند تا آن دو جمله يکسان شوند
وظيفه روتين يکسانساز Unify، گرفتن دو جمله اتمي p، q و برگرداندن يک جانشين که p، q را مشابه هم خواهد ساخت،. (اگر چنين جانشيني موجود نباشد، Unify، fail برميگرداند.)
UNIFY، عموميترين يکسانساز (Most General Unifier) يا (MGU) را برميگرداند، که جانشيني است که کمترين تعهد را در قبل محدودسازي متغيرها دارد.