Proof compression
پروف تھیوری میں، ریاضیاتی منطق کا ایک شعبہ، پروف کمپریشن رسمی ثبوتوں کو الگورتھمک طور پر کمپریس کرنے کا مسئلہ ہے۔ تیار کردہ الگورتھم کو خودکار تھیوریم ثابت کرنے والے ٹولز جیسے ایس اے ٹی حل کرنے والے، ایس ایم ٹی حل کرنے والے، فرسٹ آرڈر تھیوریم پروور اور پروف اسسٹنٹ کے ذریعے تیار کردہ ثبوتوں کو بہتر بنانے کے لیے استعمال کیا جا سکتا ہے۔ دشواری کی نمائندگی تجویز کردہ منطق میں شق سی کے ایک سیٹ سے کسی شق کا ریزولوشن ثبوت ایک ڈائریکٹڈ ایسائکلک گراف (ڈی اے جی) ہوتا ہے: ان پٹ نوڈس محوری نتائج ہوتے ہیں (احاطے کے بغیر) جن کے نتائج سی کے عناصر ہوتے ہیں، ریزولوینٹ نوڈس ریزولوشن کے نتائج ہوتے ہیں، اور ثبوت میں نتیجہ کے ساتھ ایک نوڈ ہوتا ہے۔ ڈی اے جی میں نوڈ سے نوڈ تک کا ایک کنارہ ہوتا ہے اگر اور صرف اس صورت میں جب اس کی بنیاد کا نتیجہ ہو۔ اس صورت میں، اس کا بچہ ہے، اور اس کا والدین ہے۔ ایک نوڈ جس میں بچے نہیں ہیں وہ جڑ ہے۔ ایک پروف کمپریشن الگورتھم کم نوڈس کے ساتھ ایک نیا ڈی اے جی بنانے کی کوشش کرے گا جو درست ثبوت کی نمائندگی کرتا ہے یا، کچھ معاملات میں، اس کے ذیلی سیٹ کا درست ثبوت ہے۔ ایک سادہ سی مثال آئیے شقوں کے سیٹ سے شق کے لیے قرارداد کا ثبوت لیتے ہیں۔ یہاں ہم دیکھ سکتے ہیں: اور ان پٹ نوڈس ہیں۔ نوڈ میں ایک محور ہوتا ہے، بائیں حل شدہ لفظی دائیں حل شدہ لفظی نتیجہ یہ ہے کہ شق کا احاطہ نوڈس کا اختتام ہے اور (اس کے والدین) ڈی اے جی ہوگا اور اس کے والدین ہوں گے اور ثبوت اے کی جڑ ہے (قرارداد) سی کی تردید سی سے قرارداد کا ثبوت ہے۔ یہ ایک عام نوڈ ہے، شق یا شق کا حوالہ دینے کے لیے جس کا مطلب نتیجہ شق ہے، اور (ذیلی) ثبوت جس کا مطلب ہے (ذیلی) ثبوت جس کا واحد جڑ ہے۔ کچھ کاموں میں حل کے نتائج کی الجبرائی نمائندگی پائی جا سکتی ہے۔ کے اور محور کے ساتھ ریزولوینٹ کو اس طرح ظاہر کیا جا سکتا ہے۔ جب محور کو منفرد طور پر بیان کیا جاتا ہے یا غیر متعلقہ ہوتا ہے، تو ہم اسے چھوڑ دیتے ہیں اور آسانی سے لکھتے ہیں۔ اس طرح، شقوں کے سیٹ کو کمیونیٹیٹو آپریٹر کے ساتھ الجبرا کے طور پر دیکھا جا سکتا ہے ؛ اور متعلقہ اصطلاح الجبرا میں اصطلاحات ایک نوٹیشن سٹائل میں ریزولوشن پروف کی نشاندہی کرتی ہیں جو معمول کے گراف نوٹیشن کے مقابلے میں ریزولوشن پروف کو بیان کرنے کے لیے زیادہ کمپیکٹ اور زیادہ آسان ہے۔ ہماری آخری مثال میں ڈی اے جی کا اشارہ ہوگا یا صرف ہم شناخت کر سکتے ہیں۔ کمپریشن الگورتھم ترتیب وار کیلکولس ثبوتوں کے کمپریشن کے لیے الگورتھم میں کٹ تعارف اور کٹ کا خاتمہ شامل ہیں۔ پروپوزیشنل ریزولوشن پروفز کے کمپریشن کے لیے الگورتھم میں ری سائیکل یونٹس، ری سائیکل پیوٹس، ری سائیکل پیوٹس ویتھ انٹرسیکشن، لوئر یونٹس، لوئر یونیولینٹس، اسپلٹ، ریڈیوس اینڈ ری کنسٹرکٹ، اور سبسمپشن شامل ہیں۔ نوٹوں کا ثبوت نظریہ