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

رِزولوشن (به انگلیسی: Resolution) در منطق ریاضی و اثبات قضیه خودکار، یک نوع قاعده استنتاج است. رزلوشن منجر به یک نوع فن اثبات قضیه از نوع باطل‌سازی برای جمله‌ها در منطق گزاره‌ای و منطق مرتبه اول می‌گردد؛ یعنی اگر قاعده رزلوشن را چندین بار و به صورت مناسب اعمال کنیم، می‌توانیم بگوییم که «آیا یک فرمول گزاره‌ای صادق هست»، و یا اثبات کنیم که «یک فرمول مرتبه اول صادق نیست». تلاش برای اثبات آنکه یک فرمول مرتبه‌اول صادق نیست می‌تواند منجر به محاسبات بی‌پایان بشود؛ اما در منطق گزاره‌ای این مشکل وجود ندارد.

قاعده رزلوشن را می‌توان به کارهای دیویس و پاتنم در سال ۱۹۶۰ نسبت داد؛ با این حال، در الگوریتم آن‌ها نیاز بود که «همه» نمونه‌های زمینه‌ای برای فرمول داده شده را آزمایش کرد. این منبع انفجار ترکیب‌ها در سال ۱۹۶۵ و توسط الگوریتم یکسان‌سازی نحوی جان الان رابینسون از بین رفت. در این الگویتم، امکان نمونه‌برداری از فرمول در مدت اثبات «در موقع تقاضا» فراهم بود، این نمونه‌برداری فقط تا آنجا بود که کامل‌بودن باطل‌سازی حفظ شود.

به بند ایجاد شده توسط قاعده رزلوشن، جواب (به انگلیسی: resolvent) هم می‌گویند.

رزلوشن در منطق ریاضی راهی است برای اثبات قضیه خودکار که در حساب گزاره‌ای و منطق مرتبه اول کاربرد دارد.

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

رزلوشن در منطق گزاره‌ای

قاعده رزلوشن

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

یک مکمل برای

c

در نظر گرفته می‌شود). بند نتیجه‌شده شامل همه لیترال‌هایی است که مکمل ندارند. به صورت صوری:

${\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 }}$

که در آن همه

a_{i}

،

b_{i}

ها، و

c

لیترال هستند.

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

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

${\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) اعمال می‌گردد.

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

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

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

معادل است با:

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

فن رزلوشن

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

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

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

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

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

یک مثال ساده

${\frac {a\vee b,\quad \neg a\vee c}{b\vee c}}$

در زبان ساده: فرض کنید

a

نادرست باشد. برای آنکه فرضیه

a\vee b

درست باشد،

b

باید درست باشد. از سوی دیگر، فرض کنید که

a

درست است. برای آنکه فرضیه

\neg a\vee c

درست باشد،

c

باید درست باشد؛ بنابراین، صرف‌نظر از نادرستی یا درستی

a

، اگر هر دو فرضیه برقرار باشند، آنوقت نتیجه

b\vee c

درست است.

رزلوشن در منطق مرتبه اول

قاعده رزلوشن را می‌توان به منطق مرتبه اول تعمیم داد:

${\frac {\Gamma _{1}\cup \left\{L_{1}\right\}\,\,\,\,\Gamma _{2}\cup \left\{L_{2}\right\}}{(\Gamma _{1}\cup \Gamma _{2})\phi }}\phi$

که در آن $\phi$

عمومی‌ترین یکسان‌ساز برای

L_{1}

و

{\overline {L_{2}}}

، و

\Gamma _{1}

و

\Gamma _{2}

هیچ متغیر مشترکی ندارند.

پانویس

↑ Martin Davis, Hilary Putnam (1960). "A Computing Procedure for Quantification Theory". J. ACM. 7 (3): 201–215. doi:10.1145/321033.321034. Here: p. 210, "III. Rule for Eliminating Atomic Formulas".
↑ J.A. Robinson (Jan 1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253.
↑ D.E. Knuth, The Art of Computer Programming 4A: Combinatorial Algorithms, part 1, p. 539
↑ Leitsch, Alexander (1997), The resolution calculus, EATCS Monographs in Theoretical Computer Science, Springer, p. 11, Before applying the inference method itself, we transform the formulas to quantifier-free conjunctive normal form.
↑ Enrique P. Arís, Juan L. González y Fernando M. Rubio, Lógica Computacional, Thomson, (2005).

منابع

مشارکت‌کنندگان ویکی‌پدیا. «Resolution (logic)». در دانشنامهٔ ویکی‌پدیای انگلیسی، بازبینی‌شده در ۲۹ فروردین ۱۴۰۰.

[1] Martin Davis, Hilary Putnam (1960). "A Computing Procedure for Quantification Theory". J. ACM. 7 (3): 201–215. doi:10.1145/321033.321034. Here: p. 210, "III. Rule for Eliminating Atomic Formulas".

[2] J.A. Robinson (Jan 1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253.

[3] D.E. Knuth, The Art of Computer Programming 4A: Combinatorial Algorithms, part 1, p. 539

[leitsch-4] Leitsch, Alexander (1997), The resolution calculus, EATCS Monographs in Theoretical Computer Science, Springer, p. 11, Before applying the inference method itself, we transform the formulas to quantifier-free conjunctive normal form.

[5] Enrique P. Arís, Juan L. González y Fernando M. Rubio, Lógica Computacional, Thomson, (2005).