رزولوشن (منطق)
رِزولوشن در منطق ریاضی و اثبات قضیه خودکار، یک نوع قاعده استنتاج است. رزلوشن منجر به یک نوع فن اثبات قضیه از نوع باطل‌سازی برای جمله‌ها در منطق گزاره‌ای و منطق مرتبه اول می‌گردد؛ یعنی اگر قاعده رزلوشن را چندین بار و به صورت مناسب اعمال کنیم، می‌توانیم بگوییم که «آیا یک فرمول گزاره‌ای صادق هست»، و یا اثبات کنیم که «یک فرمول مرتبه اول صادق نیست». تلاش برای اثبات آنکه یک فرمول مرتبه‌اول صادق نیست می‌تواند منجر به محاسبات بی‌پایان بشود؛ اما در منطق گزاره‌ای این مشکل وجود ندارد.
قاعده رزلوشن را می‌توان به کارهای دیویس و پاتنم در سال ۱۹۶۰ نسبت داد؛ با این حال، در آن‌ها نیاز بود که «همه» برای فرمول داده شده را آزمایش کرد. این منبع انفجار ترکیب‌ها در سال ۱۹۶۵ و توسط الگوریتم یکسان‌سازی نحوی از بین رفت. در این الگویتم، امکان نمونه‌برداری از فرمول در مدت اثبات «در موقع تقاضا» فراهم بود، این نمونه‌برداری فقط تا آنجا بود که کامل‌بودن باطل‌سازی حفظ شود.
به بند ایجاد شده توسط قاعده رزلوشن، جواب هم می‌گویند.
رزلوشن در منطق ریاضی راهی است برای اثبات قضیه خودکار که در حساب گزاره‌ای و منطق مرتبه اول کاربرد دارد.
اهمیت رزولوشن در این است که الگوریتم‌هایش کامل است یعنی با دریافت واقعیت‌هایی از جهان یا مسئله مورد نظر می‌تواند راه حل یا پاسخ را در صورت وجود بیابد.
یک قاعده رزلوشن در منطق گزاره‌ای یک قاعده استنتاج درست و منفرد است که یک بند جدید را، به عنوان پیامد برای دو بند ورودی شامل لیترال‌های مکمل می‌سازد. یک لیترال یک متغیر گزاره‌ای یا نقیض یک متغیر گزاره‌ای است. موقعی دو لیترال مکمل هستند که "یکی نقیض دیگری باشد" (در زیر formula_1 یک مکمل برای formula_2 در نظر گرفته می‌شود). بند نتیجه‌شده شامل همه لیترال‌هایی است که مکمل ندارند. به صورت صوری:
formula_3 رزلوشن بالا را می‌توان به صورت زیر هم نوشت:
formula_7
به بند تولید شده توسط قاعده رزلوشن، جواب برای دو بند ورودی هم می‌گویند. اصل اجماع به بندها و نه اصطلاح‌ها (term) اعمال می‌گردد.
موقعی که دو بند شامل بیش از یک جفت لیترال مکمل باشند، قاعده رزلوشن را می‌توان (به صورت مستقل) برای هر جفت به کار برد؛ با این حال، نتیجه همیشه همان‌گویی دارد.
وضع مقدم را می‌توان نوع خاصی رزلوشن درنظرگرفت (از یک بند تک لیترالی و یک بند دو لیترالی).
formula_8
معادل است با:
formula_9
موقعی که رزلوشن با یک الگوریتم جستجوی کامل همراه گردد، قاعده رزلوشن منجر به یک الگوریتم استوار و کامل برای تصمیم‌گیری در مورد صداقت یک فرمول گزاره‌ای می‌شود، و با گسترش آن، اعتبار یک جمله تحت نظر مجموعه‌ای از بنداشت‌ها می‌شود.
این فن رزلوشن از برهان خلف استفاده می‌کند، و بر اساس این واقعیت است که هر جمله در منطق گزاره‌ای را می‌توان به یک جمله معادل در حالت نرمال عطفی تبدیل نمود. گام‌های این فن این‌گونه اند:
نمونه ای از این الگوریتم، اصلی است، که بعدها به صورت تصفیه شد، در این نوع تصفیه‌ای نیاز برای «نمایش صریح جواب‌ها» حذف شده است.
این توصیف فن رزلوشن از یک «مجموعه "S»"، به عنوان ساختمان داده زیربنایی برای نمایش شاخه‌های رزلوشنی استفاده می‌کند. لیست‌ها، درخت‌ها، و گراف‌های بدون‌دور سودار، دیگر جایگزین‌های معمول و ممکن هستند. نمایش درختی به این واقعیت که قاعده رزلوشن، یک قاعده دودویی است بیشتر وفادار است. همراه با یک نماد ترتیبی برای بندها، یک «نمایش درختی» این موضوع را روشن می‌سازد که «چگونه قاعده رزلوشن به حالت خاصی از "" مرتبط است»، و به فرمول‌های برش اتمی محدود می‌شود. با این حال، نمایش‌های درختی به اندازه نمایش‌های مجموعه‌ای یا لیستی فشرده نیستند، زیرا به صورت صریح زیرشاخه‌های استنتاجی «زاید» برای بندهایی که بیش از یکبار در استنتاج بند خالی استفاده شده‌اند را نمایش می‌دهند. نمایش‌های گرافی می‌توانند از نظر تعداد بندها به اندازه نمایش‌های لیستی فشرده باشند، و آن‌ها همچنین "اطلاعات ساختاری" دربارهٔ اینکه «کدام بند برای اسنتاج هر جواب حل شده‌است» را ذخیره‌سازی کنند.
formula_12 در زبان ساده: فرض کنید formula_13 نادرست باشد. برای آنکه فرضیه formula_14 درست باشد، formula_15 باید درست باشد. از سوی دیگر، فرض کنید که formula_13 درست است. برای آنکه فرضیه formula_17 درست باشد، formula_2 باید درست باشد؛ بنابراین، صرف‌نظر از نادرستی یا درستی formula_13، اگر هر دو فرضیه برقرار باشند، آنوقت نتیجه formula_20 درست است.
قاعده رزلوشن را می‌توان به منطق مرتبه اول تعمیم داد:
formula_21
که در آن formula_22 عمومی‌ترین یکسان‌ساز برای formula_23 و formula_24، و formula_25 و formula_26 هیچ متغیر مشترکی ندارند.