Resolution proof reduction via local context rewriting
پروف تھیوری میں، ریاضیاتی منطق کا ایک شعبہ، مقامی سیاق و سباق کی دوبارہ تحریر کے ذریعے ریزولوشن پروف میں کمی مقامی سیاق و سباق کی دوبارہ تحریر کے ذریعے ریزولوشن پروف میں کمی کی ایک تکنیک ہے۔ اس پروف کمپریشن طریقہ کو ریڈیوس اینڈ ری کنسٹرکٹ نامی الگورتھم کے طور پر پیش کیا گیا تھا، جو ریزولوشن پروف کی پوسٹ پروسیسنگ کے طور پر کام کرتا ہے۔ ریڈیوس اینڈ ری کنسٹرکٹ مقامی ثبوت دوبارہ لکھنے کے اصولوں کے ایک سیٹ پر مبنی ہے جو ذیلی ثبوت کو مساوی یا مضبوط میں تبدیل کرتا ہے۔ ہر اصول کو ایک مخصوص سیاق و سباق سے ملنے کے لیے بیان کیا گیا ہے۔ سیاق و سباق میں دو محور (اور) اور پانچ شقیں (،،، اور) شامل ہیں۔ سیاق و سباق کی ساخت () میں دکھائی گئی ہے۔ نوٹ کریں کہ اس کا مطلب یہ ہے کہ یہ اور میں موجود ہے (مخالف قطعیت کے ساتھ) اور اور میں موجود ہے (مخالف قطعیت کے ساتھ بھی)۔ نیچے دیا گیا جدول سیمون اور دیگر کی طرف سے تجویز کردہ دوبارہ لکھنے کے قوانین کو ظاہر کرتا ہے۔ الگورتھم کا خیال ان اصولوں کو موقع پر لاگو کرکے ثبوت کے سائز کو کم کرنا ہے۔ پہلے پانچ قواعد پہلے کے ایک مقالے میں متعارف کرائے گئے تھے۔ اس کے علاوہ: قاعدہ A2 اپنے طور پر کوئی کمی نہیں کرتا ہے۔ تاہم، یہ اب بھی مفید ہے، اس کے "شفلنگ" اثر کی وجہ سے جو دوسرے اصولوں کو لاگو کرنے کے نئے مواقع پیدا کر سکتا ہے۔ قاعدہ A1 عملی طور پر استعمال نہیں کیا جاتا ہے، کیونکہ اس سے ثبوت کا سائز بڑھ سکتا ہے۔ قواعد B1، B2، B2 'اور B3 کمی کے لیے براہ راست ذمہ دار ہیں، کیونکہ وہ اصل سے زیادہ مضبوط روٹ کلاز تیار کرتے ہیں۔ B اصول کا اطلاق غیر قانونی ثبوت کا باعث بن سکتا ہے (نیچے دی گئی مثال دیکھیں)، کیونکہ روٹ کلاز میں غائب کچھ لفظی ثبوت کے راستے میں کسی اور ریزولوشن مرحلے میں شامل ہو سکتے ہیں۔ لہذا، جب ایسا ہوتا ہے تو الگورتھم کو قانونی ثبوت کی "تعمیر نو" بھی کرنی پڑتی ہے۔ مندرجہ ذیل مثال ایک ایسی صورتحال کو ظاہر کرتی ہے جہاں B2 'قاعدہ کے اطلاق کے بعد ثبوت غیر قانونی ہو جاتا ہے: نمایاں سیاق و سباق پر قاعدہ B2 کا اطلاق: ثبوت اب غیر قانونی ہے کیونکہ لفظی طور پر تبدیل شدہ جڑ شق سے غائب ہے۔ ثبوت کو دوبارہ تشکیل دینے کے لیے، کوئی بھی آخری ریزولوشن مرحلے کے ساتھ مل کر ہٹا سکتا ہے (جو اب بے کار ہے)۔ حتمی نتیجہ مندرجہ ذیل قانونی (اور مضبوط) ثبوت ہے: قاعدہ B2 'کو لاگو کرنے کا ایک نیا موقع پیدا کرنے کے لیے قاعدہ A2 کو لاگو کرکے اس ثبوت میں مزید کمی۔ عام طور پر ایسے سیاق و سباق کی ایک بہت بڑی تعداد ہوتی ہے جہاں قاعدہ A2 کا اطلاق کیا جا سکتا ہے، اس لیے ایک مکمل نقطہ نظر عام طور پر ممکن نہیں ہے۔ ایک تجویز یہ ہے کہ ریڈیوس اینڈ ری کنسٹرکٹ کو دو اختتامی معیار کے ساتھ ایک لوپ کے طور پر انجام دیا جائے: تکرار کی تعداد اور ٹائم آؤٹ (جو پہلے پہنچ جاتا ہے)۔ نیچے دیا گیا سڈو کوڈ اسے ظاہر کرتا ہے۔ 1 فنکشن ریڈیوس اینڈ ری کنسٹرکٹ (/* ایک ثبوت * /، ٹائم لمٹ، زیادہ سے زیادہ تکرار): i = 1 کے لیے 2 سے زیادہ سے زیادہ تکرار کریں 3 ریڈیوس اینڈ ری کنسٹرکٹ لوپ () کریں ؛ 4 اگر وقت> ٹائم لمٹ ہو تو// ٹائم آؤٹ 5 وقفہ ؛ 7 اینڈ فنکشن کے لیے 6 اینڈ ریڈیوس اینڈ ری کنسٹرکٹ فنکشن ریڈیوس اینڈ ری کنسٹرکٹ لوپ کا استعمال کرتا ہے، جو ذیل میں بیان کیا گیا ہے۔ الگورتھم کا پہلا حصہ ریزولوشن گراف کی ٹپوولوجیکل ترتیب دیتا ہے (اس بات پر غور کرتے ہوئے کہ کناروں کو انٹیسیڈینٹس سے ریزولوینٹس تک جاتا ہے)۔ یہ اس بات کو یقینی بنانے کے لیے کیا جاتا ہے کہ ہر نوڈ کا دورہ اس کے ماضی کے بعد کیا جائے (اس طرح، ٹوٹے ہوئے ریزولوشن کے اقدامات ہمیشہ پائے جاتے ہیں اور طے کیے جاتے ہیں)۔ 1 فنکشن ریڈیوس اینڈ ری کنسٹرکٹ لوپ (/* ایک ثبوت */): 2 ٹی ایس = ٹوپوولوجیکل چھانٹنا () ؛ ٹی ایس 4 میں ہر نوڈ کے لیے 3 اگر پتی نہیں ہے تو 5 اگر اور پھر 6 = ریزولوشن (،) ؛ 7 کے بائیں سیاق و سباق کا تعین کریں، اگر کوئی ہے تو ؛ 8 کے صحیح سیاق و سباق کا تعین کریں، اگر کوئی ہے تو ؛ 9 ہیورسٹک طور پر ایک سیاق و سباق کا انتخاب کریں (اگر کوئی ہے) اور اسی اصول کو لاگو کریں ؛ 10 اور پھر 11 کے ساتھ متبادل بنائیں ؛ 12 اور پھر اگر اور پھر 13 کے ساتھ متبادل بنائیں ؛ 14 اور پھر 15 ہیورسٹک طور پر ایک سابقہ کا انتخاب کریں یا ؛ 16 کے ساتھ یا اس کے ساتھ متبادل بنائیں ؛ 18 اینڈ فنکشن کے لیے 17 اینڈ اگر ان پٹ پروف ٹری نہیں ہے (عام طور پر، ریزولوشن گراف ہیں) اس صورت میں، اس بات کو یقینی بنانے کے لیے کہ دوبارہ لکھنے کے اصول کا اطلاق حل کے دیگر مراحل میں مداخلت نہیں کرے گا، ایک محفوظ حل یہ ہے کہ نوڈ کی ایک کاپی بنائی جائے جس کی نمائندگی شق کے ذریعے کی جائے۔ یہ محلول ثبوت کے سائز کو بڑھاتا ہے اور ایسا کرتے وقت کچھ احتیاط کی ضرورت ہوتی ہے۔ قواعد کے انتخاب کے لیے تحقیق ایک اچھی کمپریشن کارکردگی حاصل کرنے کے لیے اہم ہے۔ سیمون اور دیگر۔ قواعد کے لیے ترجیحی ترتیب کا استعمال کریں (اگر دیئے گئے سیاق و سباق پر لاگو ہو): B2> B3> {B2 '، B1}> A1'> A2 (X> Y کا مطلب ہے کہ X کو Y پر ترجیح دی جاتی ہے)۔ تجربات سے پتہ چلتا ہے کہ صرف ریڈیوس اینڈ ری کنسٹرکٹ میں الگورتھم ری سائیکل پیوٹس کے مقابلے میں کمپریشن/ٹائم کا تناسب بدتر ہے۔ تاہم، جب کہ ری سائیکل پیوٹس کو ثبوت پر صرف ایک بار لاگو کیا جا سکتا ہے، بہتر کمپریشن پیدا کرنے کے لیے ریڈیوس اینڈ ری کنسٹرکٹ کو متعدد بار لاگو کیا جا سکتا ہے۔ ریڈیوس اینڈ ری کنسٹرکٹ اور ری سائیکل پیوٹس الگورتھم کو یکجا کرنے کی کوشش کے اچھے نتائج برآمد ہوئے ہیں۔ مثال کے طور پر سیوڈو کوڈ پروف تھیوری والے مضامین کو نوٹ کریں