استنتاج از طریق تحلیل برای منطق گزاره ای هوش مصنوعی
استنتاج از طریق تحلیل برای منطق گزاره ای هوش مصنوعی
قوانین استنتاجی که تاکنون معرفی کردیم، صحیح هستند، اما در مورد کامل بودن الگوریتم های استنتاجی که از آنها استفاده میکنند، بحث نکردیم. الگوریتم های جست وجو مثل "جست وجوی تعمیق تکراری" کامل هستند، زیرا هدف قابل دسترس را پیدا خواهند کرد. اما اگر قوانین استنتاج موجود کافی نباشند، هدف قابل دسترس نیست. یعنی هیچ اثباتی وجود ندارد که فقط از آن قوانین استنتاج استفاده کند. در این بخش، یک قانون استنتاج به نام تحلیل را بررسی میکنیم که در ترکیب با هر الگوریتم جست وجوی کامل منجر به یک الگوریتم استنتاج کامل میشود.
قانون تحلیل کامل میگوید که تحلیل دو کلاز (یعنی ترکیب فصلی لیترال ها) را گرفته، کلاز جدیدی تولید میکند که حاوی تمام لیترال های دو کلاز اصلی به جز لیترال های مکمل (یعنی یکی، نقیض دیگری است) است.
جنبه دیگری از قانون تحلیل وجود دارد: کلازی که حاصل میشود، فقط باید شامل یک کپی از هر لیترال باشد. حذف چندیدن کپی از لیترال، فاکتورگیری نام دارد. بعنوان مثال اگر (AvB) را با (Av¬B) حل کنیم، (AvA) را به دست می آوریم که به A تقلیل می یابد.
نکته عجیب در مورد قانون تحلیل این است که مبنایی برای خانواده ی رویه های استنتاج کامل است. هر ثابت کننده ی قضیه مبتنی بر تحلیل برای هر جمله α و β در منطق گزاره ای میتواند تصمیم بگیرد که آیا α بر β دلالت میکند (β نتیجه منطقی جمله α است) یا خیر.
قانون تحلیل فقط به کلازها (ترکیب فصلی لیترال ها) اعمال میشود. لذا به نظر میرسد که فقط به پایگاه های دانش و پرس و جوهای شامل کلازها مربوط میشود. پس چگونه منجر به رویه استنتاج کاملی برای منطق گزاره ای میشود؟ پاسخ این است که هر جمله از منطق گزاره ای، از نظر منطقی با یک ترکیب عطفی لیترال ها هم ارز است. جمله ای که بصورت ترکیب عطفی از ترکیبات فصلی لیترالها بیان میشود، شکل نرمال عطفی یا CNF نامیده میشود.
الگوریتم تحلیل
رویه های استنتاج مبتنی بر تحلیل، بر اساس اصل اثبات برهان خلف کار میکنند که در پستهای قبل مطرح کردیم. یعنی برای اینکه نشان دهیم KB بر α دلالت میکند یا خیر مشخص میکنیم (KBʌ¬α) ارضاپذیر نیست.
یک الگوریتم تحلیل را در زیر میبینید. ابتدا (KBʌ¬α) به CNF تبدیل میشود. سپس قانون تحلیل به کلاز کوچک حاصل اعمال میشود. هر زوجی که شامل لیترال های مکمل باشد، حل میشود تا کلاز جدیدی ایجاد گردد. اگر این کلاز قبلا د مجموعه نباشد، به آن اضافه میشود. این فرآیند ادامه می یابد تا یکی از دو مورد زیر رخ دهد:
► هیچ کلاز جدیدی وجود نداشته باشد که بتواند اضافه شود. در این مورد KB نمیتواند بر α دلالت کند (KB نمیتواند α را نتیجه دهد.)
► وقتی قنون تحلیل بر روی دو کلاز عمل میکند، کلاز تهی ا به دست میدهد که در این مورد، KB بر α دلالت می کند (KB میتواند α را نتیجه دهد.)
کلاز خالی (ترکیب فصلی بدون هیچ فاصل)، هم ارز false است، زیرا ترکیب فصلی وقتی درست است که حداقل یکی از فصل ها درست باشد. روش دیگر برای اینکه نشان دهیم کلاز تهی یک تناقض را نشان میدهد، این است که، کلاز تهی وقتی به وجود می آید که دو عبارت مکمل هم با یکدیگر حل می شوند، مثل P و ¬P.
الگوریتم تحلیل ساده برای منطق گزاره ای
در این الگوریتم تابع PL-RESOLVE مجموعه ای از تمام کلازها را نشان میدهد که با حل دو ورودی اش به دست می آید.
function PL-RESOLUTION(KB, a) returns true or false
inputs : KB, the knowledge base, a sentence in propositional logic
a, the query, a sentence in propositional logic
clauses <-- the set of clause in the CNF representation of KB ʌ ¬a
new <-- { }
loop do
for each pair of clauses Ci , Cj in clauses do
resolvents <-- PL-RESOLVE(Ci , Cj )
if resolvents contains the empty clause then return true
new <-- new U resolvents
if new زیر مجموعه clauses then return false
clauses <-- clauses U new
