موضوع مقاله: رزولوشن (منطق) | مخاطب: عمومی | لحن: دانشنامه‌ای | ساختار: عنوان، مقدمه، 3 بخش، جمع‌بندی | مقاله: | # رزولوشن (منطق) | مقدمه: رزلوشن منجر به یک نوع فن اثبات قضیه از نوع باطل‌سازی برای جمله‌ها در منطق گزاره‌ای و منطق مرتبه اول می‌گردد؛ یعنی اگر قاعده رزلوشن را چندین بار و به صورت مناسب اعمال کنیم، می‌توانیم بگوییم که «آیا یک فرمول گزاره‌ای صادق هست»، و یا اثبات کنیم که «یک فرمول مرتبه اول صادق نیست». | ## بخش 1: رزولوشن (منطق) | تلاش برای اثبات آنکه یک فرمول مرتبه‌اول صادق نیست می‌تواند منجر به محاسبات بی‌پایان بشود؛ اما در منطق گزاره‌ای این مشکل وجود ندارد. با این حال، در الگوریتم آن‌ها نیاز بود که «همه» نمونه‌های زمینه‌ای برای فرمول داده شده را آزمایش کرد. این منبع انفجار ترکیب‌ها در سال ۱۹۶۵ و توسط الگوریتم یکسان‌سازی نحوی جان الان رابینسون از بین رفت. در این الگویتم، امکان نمونه‌برداری از فرمول در مدت اثبات «در موقع تقاضا» فراهم بود، این نمونه‌برداری فقط تا آنجا بود که کامل‌بودن باطل‌سازی حفظ شود. رزلوشن در منطق ریاضی راهی است برای اثبات قضیه خودکار که در حساب گزاره‌ای و منطق مرتبه اول کاربرد دارد. اهمیت رزولوشن در این است که الگوریتم‌هایش کامل است یعنی با دریافت واقعیت‌هایی از جهان یا مسئله مورد نظر می‌تواند راه حل یا پاسخ را در صورت وجود بیابد. رزلوشن در منطق گزاره‌ای قاعده رزلوشن یک قاعده رزلوشن در منطق گزاره‌ای یک قاعده استنتاج درست و منفرد است که یک بند جدید را، به عنوان پیامد برای دو بند ورودی شامل لیترال‌های مکمل می‌سازد. موقعی دو لیترال مکمل هستند که "یکی نقیض دیگری باشد" (در زیر یک مکمل برای در نظر گرفته می‌شود). رزلوشن بالا را می‌توان به صورت زیر هم نوشت: به بند تولید شده توسط قاعده رزلوشن، جواب برای دو بند ورودی هم می‌گویند. | ## بخش 2: رزولوشن (منطق) | 539 موقعی که دو بند شامل بیش از یک جفت لیترال مکمل باشند، قاعده رزلوشن را می‌توان (به صورت مستقل) برای هر جفت به کار برد؛ با این حال، نتیجه همیشه همان‌گویی دارد. وضع مقدم را می‌توان نوع خاصی رزلوشن درنظرگرفت (از یک بند تک لیترالی و یک بند دو لیترالی). معادل است با: فن رزلوشن موقعی که رزلوشن با یک الگوریتم جستجوی کامل همراه گردد، قاعده رزلوشن منجر به یک الگوریتم استوار و کامل برای تصمیم‌گیری در مورد صداقت یک فرمول گزاره‌ای می‌شود، و با گسترش آن، اعتبار یک جمله تحت نظر مجموعه‌ای از بنداشت‌ها می‌شود. این فن رزلوشن از برهان خلف استفاده می‌کند، و بر اساس این واقعیت است که هر جمله در منطق گزاره‌ای را می‌توان به یک جمله معادل در حالت نرمال عطفی تبدیل نمود. گام‌های این فن این‌گونه اند: همه جملات موجود در پایگاه دانش و نقیض جمله‌ای که باید اثبات شود (حدس) به صورت عطفی (با "و") به هم متصل می‌شوند. جمله نتیجه شده به فرم نرمال عطفی تبدیل می‌شود، که در آن عطف‌ها به صورت عناصری در یک مجموعه (S) از بندها دیده می‌شود. قاعده رزلوشن به همه جفت بندهای ممکن که شامل لیترال‌های مکمل هستند، اعمال می‌گردد. بعد از هر کاربرد قاعده رزلوشن، جمله نتیجه‌شده با حذف لیترال‌های تکراری ساده‌سازی می‌شود. اگر اینطور نباشد و هنوز هم در مجموعه بند S موجود نباشد، به S اضافه می‌شود، و برای استنتاج‌های رزلوشن بعدی درنظر گفته می‌شود. | ## بخش 3: رزولوشن (منطق) | اگر بعد از اعمال قاعده رزلوشن، بند خالی به دست آمد، آنوقت فرمول اصلی صادق نیست (یا متناقض است)، و از این رو می‌توان نتیجه گرفت که حدس اولیه از بُنداشت‌ها پیروی می‌کند. از جهت دیگر، اگر این‌طور نباشد، بند خالی به دست نمی‌آید، و قاعده رزلوشن را نمی‌توان برای به دست آوردن بندهای جدیدتر اعمال نمود، و «حدس» یک «قضیه» برای پایگاه دانش اصلی نیست. نمونه ای از این الگوریتم، الگوریتم دیویس-پاتنام اصلی است، که بعدها به صورت الگوریتم DPLL تصفیه شد، در این نوع تصفیه‌ای نیاز برای «نمایش صریح جواب‌ها» حذف شده است. این توصیف فن رزلوشن از یک «مجموعه S»، به عنوان ساختمان داده زیربنایی برای نمایش شاخه‌های رزلوشنی استفاده می‌کند. لیست‌ها، درخت‌ها، و گراف‌های بدون‌دور سودار، دیگر جایگزین‌های معمول و ممکن هستند. نمایش درختی به این واقعیت که قاعده رزلوشن، یک قاعده دودویی است بیشتر وفادار است. همراه با یک نماد ترتیبی برای بندها، یک «نمایش درختی» این موضوع را روشن می‌سازد که «چگونه قاعده رزلوشن به حالت خاصی از "قاعده برش" مرتبط است»، و به فرمول‌های برش اتمی محدود می‌شود. با این حال، نمایش‌های درختی به اندازه نمایش‌های مجموعه‌ای یا لیستی فشرده نیستند، زیرا به صورت صریح زیرشاخه‌های استنتاجی «زاید» برای بندهایی که بیش از یکبار در استنتاج بند خالی استفاده شده‌اند را نمایش می‌دهند. نمایش‌های گرافی می‌توانند از نظر تعداد بندها به اندازه نمایش‌های لیستی فشرده باشند، و آن‌ها همچنین اطلاعات ساختاری دربارهٔ اینکه «کدام بند برای اسنتاج هر جواب حل شده‌است» را ذخیره‌سازی کنند. | ## جمع‌بندی | برای آنکه فرضیه درست باشد، باید درست باشد؛ بنابراین، صرف‌نظر از نادرستی یا درستی ، اگر هر دو فرضیه برقرار باشند، آنوقت نتیجه درست است.