راهبردهای تحلیل مرتبه اول در AI

راهبردهای تحلیل مرتبه اول در AI

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

همانند منطق گزاره ای، در تحلیل مرتبه اول لازم است، جملات به شکل نرمال عطفی (CNF) باشند، یعنی ترکیبات عطفی از کلازها باشند که در آن، هر کلاز، ترکیب فصلی لیترال ها است. لیترال ها میتوانند شامل متغیرها باشند که فرض میشود با سور عمومی مشخص شده اند.

هر جمله ای از منطق مرتبه اول میتواند به جمله ای تبدیل شود که از نظر استنتاجی هم ارز CNF است. اگر جمله اصلی ارضاپذیر نباشد، جمله CNF نیز ارضاپذیر نخواهد بود، لذا مبنایی برای اثبات از طریق برهان خلف بر روی جملات CNF در اختیار داریم. رویه مراحل تبدیل به CNF بصورت زیر است:

► حذف استلزام ها

► انتقال ¬ به داخل

► استانداردسازی متغیرها

► اسکولم سازی (فرآیند حذف سورهای وجودی)

► حذف سورهای عمومی

► توزیع v روی ʌ

 

تحلیل، تکذیب کامل است، یعنی اگر مجموعه ای از جملات ارضاناپذیر باشند، آنگاه تحلیل همیشه میتواندبه تناقض برسد. تحلیل نمیتواند برای تولید تمام نتایج منطقی مجموعه ای از جملات به کار رود، ولی میتواند ثابت کند که جمله خاصی توسط مجموعه ای از جملات به دست آمده است.

 

استراتژی های تحلیل مرتبه اول

کاربردهای تکراری قانون استنتاج تحلیل، در صورت وجود اثبات آن را می یابد. در این جا استراتژی هایی را بررسی میکنیم که به یافتن کارآمد کمک میکند.

♦ استراتژی ترجیح واحد

این استراتژی در جایی که جملات فقط یک لیترال هستند، ترجیح میدهد از تکنیک تحلیل استفاده کند (این جملات را کلاز واحد می نامند.) ایده ی ورای این استراتژی این است که سعی میکنیم کلاز خالی را ایجاد کنیم. لذا خوب است به استنتاج هایی اولویت داده شود که کلازهای کوتاه تری دارند.

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

 

♦ استراتژی مجموعه پشتیبان

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

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

 

♦ استراتژی تحلیل ورودی

در استراتژی تحلیل ورودی، هر تحلیل یکی از جملات ورودی (از KB یا پرس وجو) را با جمله دیگری ترکیب میکند. در پایگاه های دانش هرون، استنتاج قیاسی نوعی راهبرد تحلیل ورودی است، زیرا استلزامی از  KB اصلی را با جملات دیگر ترکیب میکند. لذا تعجبی ندارد که تحلیل ورودی برای پایگاه های دانش به شکل هورن، کامل باشد.

اما این استراتژی در حالت کلی کامل نیست. راهبرد تحلیل خطی تعمیمی است که اجازه میدهد P و Q با هم حل شوند، اگر P در KB اصلی باشد یا P در جدّ Q در درخت اثبات باشد، تحلیل خطی کامل است.

 

♦ راهبرد شمول

روش شمول تمام جملاتی را حذف میکند که از جمله موجود در KB استنتاج میشود. شمول موجب میشود تا KB کوچک بماند و د نتیجه فضای جست وجو کوچک خواهد شد.