(به : ) در و ، یک نوع است. رزلوشن منجر به یک نوع فن از نوع برای جمله‌ها در و می‌گردد؛ یعنی اگر قاعده رزلوشن را چندین بار و به صورت مناسب اعمال کنیم، می‌توانیم بگوییم که «آیا یک صادق هست»، و یا اثبات کنیم که «یک فرمول مرتبه اول صادق نیست». تلاش برای اثبات آنکه یک فرمول مرتبه‌اول صادق نیست می‌تواند منجر به محاسبات بی‌پایان بشود؛ اما در منطق گزاره‌ای این مشکل وجود ندارد.
 قاعده رزلوشن را می‌توان به کارهای و در سال ۱۹۶۰ نسبت داد؛ با این حال، در آن‌ها نیاز بود که «همه» برای فرمول داده شده را آزمایش کرد. این منبع انفجار ترکیب‌ها در سال ۱۹۶۵ و توسط نحوی از بین رفت. در این الگویتم، امکان نمونه‌برداری از فرمول در مدت اثبات «در موقع تقاضا» فراهم بود، این نمونه‌برداری فقط تا آنجا بود که حفظ شود. 
 به بند ایجاد شده توسط قاعده رزلوشن، (به : ) هم می‌گویند.
 رزلوشن در راهی است برای که در و کاربرد دارد.
 اهمیت رزولوشن در این است که الگوریتم‌هایش کامل است یعنی با دریافت واقعیت‌هایی از جهان یا مسئله مورد نظر می‌تواند راه حل یا پاسخ را در صورت وجود بیابد.
 یک در منطق گزاره‌ای یک قاعده استنتاج درست و منفرد است که یک جدید را، به عنوان پیامد برای دو بند ورودی شامل لیترال‌های مکمل می‌سازد. یک یک متغیر گزاره‌ای یا نقیض یک متغیر گزاره‌ای است. موقعی دو لیترال مکمل هستند که "یکی نقیض دیگری باشد" (در زیر یک مکمل برای در نظر گرفته می‌شود). بند نتیجه‌شده شامل همه لیترال‌هایی است که مکمل ندارند. به صورت صوری:
 
 
 رزلوشن بالا را می‌توان به صورت زیر هم نوشت:
 
 به بند تولید شده توسط قاعده رزلوشن، برای دو بند ورودی هم می‌گویند. اصل به بندها و نه اصطلاح‌ها (term) اعمال می‌گردد. 
 موقعی که دو بند شامل بیش از یک جفت لیترال مکمل باشند، قاعده رزلوشن را می‌توان (به صورت مستقل) برای هر جفت به کار برد؛ با این حال، نتیجه همیشه دارد.
 را می‌توان نوع خاصی رزلوشن درنظرگرفت (از یک بند تک لیترالی و یک بند دو لیترالی).
 
 معادل است با:
 
 موقعی که رزلوشن با یک کامل همراه گردد، قاعده رزلوشن منجر به یک الگوریتم و برای در مورد صداقت یک فرمول گزاره‌ای می‌شود، و با گسترش آن، یک جمله تحت نظر مجموعه‌ای از بنداشت‌ها می‌شود.
 این فن رزلوشن از استفاده می‌کند، و بر اساس این واقعیت است که هر جمله در منطق گزاره‌ای را می‌توان به یک جمله معادل در تبدیل نمود. گام‌های این فن این‌گونه اند:
 
 
 
 
 نمونه ای از این الگوریتم، اصلی است، که بعدها به صورت تصفیه شد، در این نوع تصفیه‌ای نیاز برای «نمایش صریح جواب‌ها» حذف شده است.
 این توصیف فن رزلوشن از یک «مجموعه ، به عنوان زیربنایی برای نمایش شاخه‌های رزلوشنی استفاده می‌کند. ، ، و ، دیگر جایگزین‌های معمول و ممکن هستند. نمایش درختی به این واقعیت که قاعده رزلوشن، یک قاعده دودویی است بیشتر وفادار است. همراه با یک نماد ترتیبی برای بندها، یک «نمایش درختی» این موضوع را روشن می‌سازد که «چگونه قاعده رزلوشن به حالت خاصی از " " مرتبط است»، و به فرمول‌های برش اتمی محدود می‌شود. با این حال، نمایش‌های درختی به اندازه نمایش‌های مجموعه‌ای یا لیستی فشرده نیستند، زیرا به صورت صریح زیرشاخه‌های استنتاجی «زاید» برای بندهایی که بیش از یکبار در استنتاج بند خالی استفاده شده‌اند را نمایش می‌دهند. نمایش‌های گرافی می‌توانند از نظر تعداد بندها به اندازه نمایش‌های لیستی فشرده باشند، و آن‌ها همچنین دربارهٔ اینکه «کدام بند برای اسنتاج هر جواب حل شده‌است» را ذخیره‌سازی کنند.
 
در زبان ساده: فرض کنید نادرست باشد. برای آنکه فرضیه درست باشد، باید درست باشد. از سوی دیگر، فرض کنید که درست است. برای آنکه فرضیه درست باشد، باید درست باشد؛ بنابراین، صرف‌نظر از نادرستی یا درستی ، اگر هر دو فرضیه برقرار باشند، آنوقت نتیجه درست است.
 قاعده رزلوشن را می‌توان به تعمیم داد: 
 
 که در آن برای و ، و و هیچ متغیر مشترکی ندارند.
 
 مشارکت‌کنندگان ویکی‌پدیا. « ». در ، بازبینی‌شده در ۲۹ فروردین ۱۴۰۰.
{"title": "رزولوشن (منطق)", "link": "https://fa.wikipedia.org//w/index.php?title=%D8%B1%D8%B2%D9%88%D9%84%D9%88%D8%B4%D9%86_(%D9%85%D9%86%D8%B7%D9%82)&oldid=33458225", "language": "fa"}