فصل هشتم

استنتاج در منطق مرتبه اول

1. فصل اول هوش مصنوعی Artificial Intelligence
2. فصل دوم عامل های هوشمند
3. فصل سوم حل مسائل توسط جستجو
4. فصل چهارم روش‌های جستجو آگاهانه
5. فصل 5 تئوری بازی
6. فصل ششم عامل‌هاییکه به طور منطقی استدلال می‌‌کنند
7. فصل هفتم منطق مرتبه اول
8. فصل هشتم استنتاج در منطق مرتبه اول
9. فصل نهم برنامه‌ریزی
10. فصل دهم عدم قطعیت

 

قوانین استنتاج مربوط به سورها:

قوانین استنتاج برای منطق گزاره‌ای:

Modus Ponens

And – Elimination

And – Introduction

Or – Introduction

Resolution

سه قانون استنتاجی جدید:

1- حذف سور عمومی (Universal Elimination):

برای هر جمله α متغیر v، و ترم زمینی g داریم:

2- حذف سور وجودی:

برای هر جمله α، متغیر v، و سیمبول ثابت k که جای دیگری از پایگاه دانش ظاهر نشده است، داریم:

3- (Existential Introduction):

برای هر جمله α، متغیر v که در α واقع نباشد، و ترم زمینی g‌که در α واقع نشود داریم:

می‌توان این قوانین را با استفاده از:

یک جمله با سور عمومی به عنوان ترکیب عطفی تمام مقداردهی‌های ممکن آن، و تعریف یک جمله با سور وجودی به عنوان ترکیب فصلی تمام مقداردهی‌های ممکن آن، کنترل کرد.

کاربرد قوانین استنتاج، در واقع پرسشی از مطابقت نمونه‌های پیش‌فرضیات آنها با جملات موجود در KB و سپس افزودن نمونه‌های جدید آنهاست.

اگر ما فرایند یافتن اثبات را به عنوان یک پردازش جستجو فرموله‌سازی کنیم، پس واضح است که اثبات همان راه حل مسئله جستجو است و روشن است که باید برنامه‌ای هوشمند برای یافتن اثبات بدون دنبال کردن هر گونه مسیر نادرست موجود باشد.

Modus Ponens تعمیم یافته:

• فرم Canonical
• یکسان‌سازی (Unificaiton)

فرم Canonical:

تمام جملات موجود در پایگاه دانش باید به صورتی باشند که با یکی از پیش‌فرضیات قانون Modus Ponens مطابقت داشته بشاند، فرم Canonical برای Modus Ponens متضمن این نکته است که هر جمله در پایگاه دانش از چه نوع اتمی یا شرطی با یک ترکیب عطفی از جملات اتمی در طرف چپ و یک اتم منفرد در طرف راست باید باشد.

ما جملات را به جملات Horn زمانی تبدیل می‌کنیم که ابتدا وارد پایگاه دانش، با استفاده از حذف سور وجودی و حذف And شده باشند.

یکسان‌سازی (Unificaiton):

 

وظیفه روتین یکسان‌ساز Unify، گرفتن دو جمله اتمی p، q و برگرداندن یک جانشین که p، q را مشابه هم خواهد ساخت، است. (اگر چنین جانشینی موجود نباشد، Unify، fail برمی‌گرداند.)

UNIFY، عمومی‌ترین یکسان‌ساز (Most General Unifier) یا (MGU) را برمی‌گرداند، که جانشینی است که کمترین تعهد را در قبل محدودسازی متغیرها دارد.

زنجیره‌سازی به جلو و عقب (Forward AND Backward Chaining):

زنجیره‌سازی به جلو (forward chaining):

قانون Modus Ponens تعمیم یافته به دو صورت استفاده می‌شود. می‌توانیم با جملات موجود در پایگاه دانش شروع کنیم و نتایج جدیدی را که می‌توانند استنباط‌های بیشتری را بسازند، تولید کنیم. این روش زنجیره‌سازی به جلو نامیده می‌شود.

این روش زمانی استفاده می‌شود که حقیقت جدیدی به پایگاه داده ما اضافه شده باشد و خواسته باشیم نتایج آن را تولید کنیم.

زنجیره‌سازی به عقب (Backward Chaining):

می‌توانیم با چیزی که قصد اثباتش را داریم آغاز کنیم و جملات شرطی را پیدا کنیم که به ما اجازه بدهند نتیجه را از آنها استنتاج کنیم، و سپس سعی در ایجاد پیش‌فرضیات آنها داشته باشیم.

این روش زمانی استفاده می‌شود که هدفی برای اثبات وجود داشته باشد.

الگوریتم زنجیره‌سازی به جلو:

زنجیره‌سازی به جلو توسط افزودن یک حقیقت جدید p به پایگاه دانش، فعال می‌شود و می‌تواند به عنوان قسمتی از پردازش TELL برای مثال، همکاری داشته باشد. در اینجا ایده، یافتن تمام ترکیبات شرطی است که P را به‌عنوان پیش‌فرض داشته باشد، سپس اگر بقیه پیش‌فرضیات برقرار باشند، می‌توانیم نتیجه ترکیب شرطی را به پایگاه دانش توسط راه‌اندازی استنتاج‌های بعدی اضافه کنیم.

ما به ایده ترکیب (Composition) جانشینی نیز نیاز داریم.

جانشینی است که اثر آن با اثر اعمال هر جانشینی به نوبت، برابر است. زیرا:

زنجیره‌سازی به جلو، تصویری تدریجی از شرایط در حالی که داده‌های جدید وارد می‌شوند، می‌سازد.

پردازش‌های استنتاجی آن مستقیماً با حل مسئله ویژه در ارتباط نیستند،

به همین دلیل رویه data-driven یا data-directed نامیده می‌شود.

الگوریتم زنجیره‌سازی به عقب:

زنجیره‌سازی به عقب به منظور یافتن تمام پاسخ‌ها برای سؤال طرح شده، به وجود آمده است. بنابراین زنجیره‌سازی به عقب، وظیفه‌ای که از رویه ASK خواسته شده را انجام می‌دهد. الگوریتم زنجیره‌سازی به عقب BACK-CHAIN ابتدا توسط کنترل درمی‌یابد که آیا پاسخ‌ها مستقیماً از جملات پایگاه دانش، تولید می‌شوند یا خیر. سپس تمام ترکیبات شرطی که نتایجشان با پرسش (query) مطابقت دارد را پیدا می‌کند و سعی دارد تا پیش‌فرض‌های آن ترکیبات شرطی را توسط زنجیره‌سازی به عقب ایجادکند.

اگر پیش‌فرض، یک ترکیب عطفی باشد، سپس BACK-CHAIN ترکیبات عطفی را عطف به عطف پردازش می‌کند، تا یکسان‌ساز را برای تمام پیش‌فرض بسازد.

کامل بودن Completeness:

 

تصور کنید که ما پایگاه دانش زیر را در اختیار داریم:

سپس ما می‌خواهیم که S(A) را نتیجه بگیریم، S(A) درست است،

اگر Q(A)‌یا R(A) درست باشد، و یکی از آنها باید درست باشد زیرا:

یا P(A) یا P(A) ¬ درست است.

متأسفانه، زنجیره‌سازی با Modus Ponens نمی‌تواند S(A) را نتیجه بگیرد.

مشکل این است که         نمی‌تواند به صورت Horn دربیاید، و از این رو توسط Modus Ponens نمی‌تواند استفاده شود.

این بدان معنی است که رویه اثباتی که از Modus Ponens استفاده می‌کند ناکامل (incomplete) است:

جملاتی که در پایگاه دانش مستلزم شده‌اند ولی رویه نمی‌تواند آنها را استنتاج کند.

پرسش در مورد وجود رویه‌های اثبات کامل بحثی است که ارتباط مستقیم با ریاضیات دارد. اگر یک رویه اثبات کامل بتواند برای عبارات ریاضی پیدا شود، دو چیز دنبال می‌شود:

• تمام مفروضات می‌توانند به طور مکانیکی ایجاد شوند.
• تمام ریاضیات می‌توانند به عنوان نتیجه منطقی مجموعه‌ای از اصل موضوع‌های پایه‌ای ایجاد شوند.

یک رویه اثبات کامل برای منطق مرتبه اول ارزش بسیاری در AI دارد:

• نظریه‌های عملی در رابطه با پیچیدگی کامپیوتری.
• فعال ساختن یک ماشین برای حل هر گونه مسئله که در زبان می‌تواند قرار داده شود.

قضیه کامل بودن گودل نشان داد که، برای منطق مرتبه اول، هر جمله‌ای که توسط مجموعه جملات دیگری مستلزم شود می‌تواند از آن مجموعه اثبات شود. بنابراین می‌توانیم قوانین استنتاجی را که به یک رویه اثبات کامل R اجازه می‌دهد، پیدا کنیم:

این قضیه کامل بودن مشابه این است که بگوییم رویه‌ای برای یافتن سوزنی در یک پشته کاه وجود دارد و این ادعای بیهوده نیست زیرا جملات با سود عمومی و سیمبول‌های تابع لانه‌ای دلخواهی در پشته‌های کاه با اندازه نامحدود، استفاده می‌شوند.

گودل نشان داد که رویه اثباتی وجود دارد اما هیچ رویه‌ای را ذکر نکرد.

استلزام در منطق مرتبه اول، نیمه تصمیم‌پذیر (Semidecidable) بنابراین می‌توانیم نشان دهیم که جملات از پیش‌فرضیات تبعیت می‌کنند، اما همیشه نمی‌توانیم نشان دهیم که آنها از پیش‌فرضیات تبعیت نمی‌کنند.

به‌عنوان یک فرضیه، سازگاری (consistency) مجموعه جملات (سؤالی در مورد وجود راه‌حلی برای تبدیل تمام جملات به جملات درست) نیز نیمه تصمیم‌پذیر است.

Resolution: یک رویه استنتاج کامل

از دو ترکیب شرطی می‌توانیم ترکیب سومی را مشتق کنیم که پیش‌فرض اولی را به نتیجه دومی متصل می‌کند.

Modus Ponens به ما اجازه استخراج ترکیب شرطی جدید را نمی‌دهد و فقط نتایج اتمی را استخراج می‌کند. از این رو قانون resolution قدرتمندتر از Modus Ponens است.

قانون استنتاج resolution:

 

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

Resolution  تعمیم یافته (ترکیبات فصلی)

Resolution تعمیمی یافته (ترکیبات شرطی)

Resolution‌تعمیم یافته (ترکیبات فصلی):

برای Pi و qi فرضی که UNIFY (Pj ¬ qk)=θ

معادلاً، می‌توانیم این عبارت را به صورت ترکیب شرطی بنویسیم.

Resolution تعمیم یافته (ترکیبات شرطی):

برای اتم‌های Pi و qi و ri و si که

UNIFY (Pj , qk)=θ

فرم‌های Canonical  برای resolution:

در نسخه اولیه قانون resolution، هر جمله یک ترکیب فصلی از حروف فرضی است.

تمام ترکیبات فصلی در KB فرض شده‌اند که در یک ترکیب عطفی صریح (مانند یک KB‌معمولی) به هم متصل شده‌اند، بنابراین این فرم، فرم نرمال عطفی Conjunctive normal form (CNF) نامیده می‌شود.

اگرچه هر جمله به تنهایی یک ترکیب فصلی است.

در صورت ثانویه قانون resolution، هر جمله یک ترکیب شرطی با یک ترکیب عطفی از اتم‌ها در سمت چپ و یک ترکیب فصلی از اتم‌ها در طرف راست است.

این حالت، فرم نرمال شرطی(implicative normal form (INF)  نامیده می‌شود.

هر مجموعه از جملات می‌توانند به دو فرم ترجمه شوند. فرم نرمال عطفی رایج‌تر است، اما فرم نرمال شرطی طبیعی‌تر به نظر می‌آید.

Resolution تعمیمی از Modus Ponens است.

فرم نرمال شرطی رایج‌تر از فرم Horn است، به دلیل اینکه طرف سمت راست می‌تواند یک ترکیب شرطی باشد و نه فقط یک اتم تنها.

Modus Ponens قابلیت ترکیب اتم‌ها با یک ترکیب شرطی را به منظور استخراج نتیجه به صورتی دارد که resolution قادر به انجام آن نیست.

زنجیره‌سازی با resolution قدرتمندتر از زنجیره‌سازی با Modus Ponens است، اما هنوز کامل نیست.

برهان خلف:

رویه استنتاج کاملی که از resolution استفاده می‌کند برهان خلف (refutation) نامیده می‌شود و هم‌چنین به عنوان اثبات توسط تناقض (proof by contradiction) و (reduction and absurdum شناخته شده است.

تبدیل به فرم نرمال:

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

رویه‌ای برای تبدیل به فرم نرمال:

1) حذف ترکیب شرطی:

می‌توان تمام ترکیبات شرطی را با معادل فصلی جایگزین نمود.

2) حذف ¬:

نقیض فقط برای فرم نرمال عطفی مجاز است، و برای تمام فرم‌های نرمال شرطی قدغن است.

3) استاندارد کردن متغیرها:

این عمل بعداً از ایجاد ابهام زمان حذف سورها جلوگیری می‌کند.

4) انتقال سورها به سمت چپ:

5) Skolemize:

Skolemization پردازشی است که در آن تمام سورهای وجودی حذف می‌شوند.

6) توزیع Λ بر ν :

7) ترکیبات فصلی و عطفی لانه‌ای مسطح شده:

در این مورد، جمله به فرم نرمال عطفی (CNF)‌است.

8) تبدیل ترکیبات فصلی به ترکیب شرطی:

برخورد با مسئله تساوی:

یکسان‌سازی یک تست نحوی مبتنی بر ظاهر ترم‌های آرگومانی است و تست صحیح معنایی مبتنی بر اشیایی که نمایش می‌دهند، نیست.

دو روش برای انجام این امر:

1) بدیهی نمودن تساوی به وسیله ذکر خواص آن:

باید ذکر شود که تساوی، انعطاف‌پذیر، متقارن و (متعدی) است.

2) استفاده از یک قانون استنتاج از یک قانون استنتاج:

می‌توانیم قانون استنتاج را به صورت زیر تعریف کنیم:

Demodulation: برای تمام ترم‌های z,y,x که UNIFY (x,y) = θ

استراتژی‌های Resolution:

4 استراتژی که برای راهنمایی جستجو به سمت یک اثبات استفاده می‌شوند، را بررسی خواهیم کرد:

• Unit preference:

در اینجا ما سعی بر تولید جمله کوتاهی به صورت True => False‌داریم.

این استراتژی یک کشف‌کننده مفید است که می‌تواند با دیگر استراتژی‌ها ترکیب شود.

2) مجموعه Support

هر resolution جمله‌ای را از مجموعه Support با جمله دیگری ترکیب می‌کند و نتیجه را به مجموعه Support اضافه می‌کند. اگر مجموعه Support به نسبت تمام پایگاه دانش کوچک باشد، فضای جستجو را قطع خواهد کرد.

یک انتخاب بد برای مجموعه Support الگوریتم را ناکامل خواهد ساخت.

استراتژی مجموعه Support دارای این مزیت است که درخت‌های اثباتی تولید می‌کند که اغلب برای درک افراد آسان هستند، زیرا آنها هدف‌گرا هستند.

3) Resolution‌ورودی:

در استراتژی resolution ورودی هر resolution یکی از جملات ورودی را (از KB یا query) با جمله دیگر ترکیب می‌کند.

در پایگاه‌های دانش Horn، Modus Ponens نوعی از استراتژی resolution ورودی است، زیرا یک ترکیب شرطی از KB اصلی را با دیگر جملات ترکیب می‌کند. از این رو شگفتی‌آور نخواهد بود که resolution ورودی برای پایگاه‌های دانشی که به صورت Horn هستند، کامل باشد اما در حالت کلی ناکامل است.

4) Subsumption:

متد Subsumption تمام جملاتی که توسط یک جمله موجود در KB، Subsume می‌شوند، را حذف می‌کند.

Subsumption به نگهداری KB به صورت کوچک کمک می‌کند، و در نتیجه فضای جستجو را کوچک می‌سازد.