رزولوشن (منطق)

یک قاعده رزلوشن در منطق گزاره‌ای یک قاعده استنتاج درست و منفرد است که یک بند جدید را، به عنوان پیامد برای دو بند ورودی شامل لیترال‌های مکمل می‌سازد. یک لیترال یک متغیر گزاره‌ای یا نقیض یک متغیر گزاره‌ای است. موقعی دو لیترال مکمل هستند که "یکی نقیض دیگری باشد" (در زیر ${\displaystyle \lnot c}$ یک مکمل برای ${\displaystyle c}$ در نظر گرفته می‌شود). بند نتیجه‌شده شامل همه لیترال‌هایی است که مکمل ندارند. به صورت صوری:

${\displaystyle {\frac {a_{1}\lor a_{2}\lor \cdots \lor c,\quad b_{1}\lor b_{2}\lor \cdots \lor \neg c}{a_{1}\lor a_{2}\lor \cdots \lor b_{1}\lor b_{2}\lor \cdots }}}$

که در آن همه ${\displaystyle a_{i}}$، ${\displaystyle b_{i}}$ ها، و ${\displaystyle c}$ لیترال هستند.

خط جداکننده به معنی پیامد منطقی (به انگلیسی: entails) است.

رزلوشن بالا را می‌توان به صورت زیر هم نوشت:

${\displaystyle {\frac {(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow c,\quad c\rightarrow (b_{1}\lor b_{2}\lor \cdots )}{(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow (b_{1}\lor b_{2}\lor \cdots )}}}$

به بند تولید شده توسط قاعده رزلوشن، جواب برای دو بند ورودی هم می‌گویند. اصل اجماع به بندها و نه اصطلاح‌ها (term) اعمال می‌گردد.[3]

موقعی که دو بند شامل بیش از یک جفت لیترال مکمل باشند، قاعده رزلوشن را می‌توان (به صورت مستقل) برای هر جفت به کار برد؛ با این حال، نتیجه همیشه همان‌گویی دارد.

قیاس استثنایی را می‌توان نوع خاصی رزلوشن درنظرگرفت (از یک بند تک لیترالی و یک بند دو لیترالی).

${\displaystyle {\frac {p\rightarrow q,\quad p}{q}}}$

معادل است با:

${\displaystyle {\frac {\lnot p\lor q,\quad p}{q}}}$

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

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

• همه جملات موجود در پایگاه دانش و نقیض جمله‌ای که باید اثبات شود (حدس) به صورت عطفی (با "و") به هم متصل می‌شوند.
• جمله نتیجه شده به فرم نرمال عطفی تبدیل می‌شود، که در آن عطف‌ها به صورت عناصری در یک مجموعه (S) از بندها دیده می‌شود.[4]
  • برای مثال، ${\displaystyle (A_{1}\lor A_{2})\land (B_{1}\lor B_{2}\lor B_{3})\land (C_{1})}$ به مجموعه ${\displaystyle S=\{A_{1}\lor A_{2},B_{1}\lor B_{2}\lor B_{3},C_{1}\}}$ افزایش می‌یابد.
• قاعده رزلوشن به همه جفت بندهای ممکن که شامل لیترال‌های مکمل هستند، اعمال می‌گردد. بعد از هر کاربرد قاعده رزلوشن، جمله نتیجه‌شده با حذف لیترال‌های تکراری ساده‌سازی می‌شود. اگر بند شامل لیترال‌های مکمل باشد، دور ریخته می‌شود (به عنوان همان‌گویی). اگر اینطور نباشد و هنوز هم در مجموعه بند S موجود نباشد، به S اضافه می‌شود، و برای استنتاج‌های رزلوشن بعدی درنظر گفته می‌شود.
• اگر بعد از اعمال قاعده رزلوشن، بند خالی به دست آمد، آنوقت فرمول اصلی صادق نیست (یا متناقض است)، و از این رو می‌توان نتیجه گرفت که حدس اولیه از بُنداشت‌ها پیروی می‌کند.
• از جهت دیگر، اگر این‌طور نباشد، بند خالی به دست نمی‌آید، و قاعده رزلوشن را نمی‌توان برای به دست آوردن بندهای جدیدتر اعمال نمود، و «حدس» یک «قضیه» برای پایگاه دانش اصلی نیست.

نمونه ای از این الگوریتم، الگوریتم دیویس-پاتنام اصلی است، که بعدها به صورت الگوریتم DPLL تصفیه شد، در این نوع تصفیه‌ای نیاز برای «نمایش صریح جواب‌ها» حذف شده است.

این توصیف فن رزلوشن از یک «مجموعه S»، به عنوان ساختمان داده زیربنایی برای نمایش شاخه‌های رزلوشنی استفاده می‌کند. لیست‌ها، درخت‌ها، و گراف‌های بدون‌دور سودار، دیگر جایگزین‌های معمول و ممکن هستند. نمایش درختی به این واقعیت که قاعده رزلوشن، یک قاعده دودویی است بیشتر وفادار است. همراه با یک نماد ترتیبی برای بندها، یک «نمایش درختی» این موضوع را روشن می‌سازد که «چگونه قاعده رزلوشن به حالت خاصی از "قاعده برش" مرتبط است»، و به فرمول‌های برش اتمی محدود می‌شود. با این حال، نمایش‌های درختی به اندازه نمایش‌های مجموعه‌ای یا لیستی فشرده نیستند، زیرا به صورت صریح زیرشاخه‌های استنتاجی «زاید» برای بندهایی که بیش از یکبار در استنتاج بند خالی استفاده شده‌اند را نمایش می‌دهند. نمایش‌های گرافی می‌توانند از نظر تعداد بندها به اندازه نمایش‌های لیستی فشرده باشند، و آن‌ها همچنین اطلاعات ساختاری دربارهٔ اینکه «کدام بند برای اسنتاج هر جواب حل شده‌است» را ذخیره‌سازی کنند.

${\displaystyle {\frac {a\vee b,\quad \neg a\vee c}{b\vee c}}}$ در زبان ساده: فرض کنید ${\displaystyle a}$ نادرست باشد. برای آنکه فرضیه ${\displaystyle a\vee b}$ درست باشد، ${\displaystyle b}$ باید درست باشد. از سوی دیگر، فرض کنید که ${\displaystyle a}$ درست است. برای آنکه فرضیه ${\displaystyle \neg a\vee c}$ درست باشد، ${\displaystyle c}$ باید درست باشد؛ بنابراین، صرف‌نظر از نادرستی یا درستی ${\displaystyle a}$، اگر هر دو فرضیه برقرار باشند، آنوقت نتیجه ${\displaystyle b\vee c}$ درست است.