Proof compression
প্রুফ থিওরিতে, গাণিতিক যুক্তির একটি ক্ষেত্র, প্রুফ কম্প্রেশন হল আনুষ্ঠানিক প্রমাণগুলিকে অ্যালগরিদমিকভাবে সংকুচিত করার সমস্যা। উন্নত অ্যালগরিদমগুলি এস. এ. টি সমাধানকারী, এস. এম. টি-সমাধানকারী, প্রথম-ক্রম উপপাদ্য প্রমাণকারী এবং প্রমাণ সহকারীদের মতো স্বয়ংক্রিয় উপপাদ্য প্রমাণকারী সরঞ্জাম দ্বারা উত্পন্ন প্রমাণগুলিকে উন্নত করতে ব্যবহার করা যেতে পারে। সমস্যা উপস্থাপনা প্রস্তাবনা যুক্তিতে 'সি' ধারার একটি সেট থেকে একটি ধারার রেজোলিউশন প্রমাণ হল একটি নির্দেশিত অ্যাসাইক্লিক গ্রাফ (ডিএজি): ইনপুট নোডগুলি স্বতঃসিদ্ধ অনুমান (প্রাঙ্গণ ছাড়াই) যার সিদ্ধান্তগুলি 'সি'-এর উপাদান, রেজোলিউশন নোডগুলি রেজোলিউশন অনুমান এবং প্রমাণটির উপসংহার সহ একটি নোড রয়েছে। ডিএজি-তে একটি নোড থেকে একটি নোড পর্যন্ত একটি প্রান্ত থাকে যদি এবং শুধুমাত্র যদি এর একটি ভিত্তি এর উপসংহার হয়। এই ক্ষেত্রে, একটি সন্তান, এবং এর পিতামাতা। একটি নোড যার কোনও সন্তান নেই এটি একটি মূল। একটি প্রুফ কম্প্রেশন অ্যালগরিদম কম নোড সহ একটি নতুন ডিএজি তৈরি করার চেষ্টা করবে যা একটি বৈধ প্রমাণ বা কিছু ক্ষেত্রে, এর একটি উপসেটের বৈধ প্রমাণ উপস্থাপন করে। একটি সহজ উদাহরণ আসুন ধারাগুলির সেট থেকে ধারাটির জন্য একটি রেজোলিউশন প্রমাণ নেওয়া যাক এখানে আমরা দেখতে পারিঃ এবং ইনপুট নোড। নোডের একটি পিভট রয়েছে, বাম সমাধান করা আক্ষরিক ডান সমাধান করা আক্ষরিক উপসংহার হল ধারা প্রাঙ্গণটি নোডের উপসংহার এবং (এর পিতামাতা) ডিএজি হবে এবং এর পিতামাতা একটি শিশু এবং প্রমাণের মূল এ (রেজোলিউশন) সি-এর প্রত্যাখ্যান সি থেকে একটি রেজোলিউশন প্রমাণ। এটি একটি সাধারণ প্রদত্ত নোড, যা ধারা বা এর ধারা বোঝায় যার অর্থ উপসংহার ধারা, এবং (উপ) প্রমাণ যার অর্থ (উপ) প্রমাণ তার একমাত্র মূল হিসাবে রয়েছে। কিছু রচনায় রেজোলিউশন অনুমানের একটি বীজগাণিতিক উপস্থাপনা পাওয়া যায়। পিভটের সাথে এবং এর সমাধানকারীকে হিসাবে চিহ্নিত করা যেতে পারে। যখন পিভটটি অনন্যভাবে সংজ্ঞায়িত বা অপ্রাসঙ্গিক হয়, তখন আমরা এটি বাদ দিয়ে সহজভাবে লিখি। এইভাবে, ধারাগুলির সেটকে একটি বিনিময়কারী অপারেটর সহ বীজগণিত হিসাবে দেখা যেতে পারে; এবং সংশ্লিষ্ট শব্দ বীজগণিতের পদগুলি একটি স্বরলিপি শৈলীতে রেজোলিউশন প্রমাণকে বোঝায় যা স্বাভাবিক গ্রাফ স্বরলিপির তুলনায় রেজোলিউশন প্রমাণ বর্ণনা করার জন্য আরও সংক্ষিপ্ত এবং আরও সুবিধাজনক। আমাদের শেষ উদাহরণে ডিএজি-র স্বরলিপি হবে বা সহজভাবে আমরা সনাক্ত করতে পারি। কম্প্রেশন অ্যালগরিদম ক্রমিক ক্যালকুলাস প্রমাণের সংকোচনের জন্য অ্যালগরিদমগুলির মধ্যে রয়েছে কাটা ভূমিকা এবং কাটা অপসারণ। প্রস্তাবনাগত রেজোলিউশন প্রমাণের সংকোচনের জন্য অ্যালগরিদমগুলির মধ্যে রয়েছে পুনর্ব্যবহারযোগ্য ইউনিট, পুনর্ব্যবহারযোগ্য ইউনিট, পুনর্ব্যবহারযোগ্য ইউনিট, পুনর্ব্যবহারযোগ্য ইউনিট, নিম্ন ইউনিট, নিম্ন ইউনিট, বিভাজন, হ্রাস ও পুনর্গঠন এবং সাবসাম্পশন। নোটের প্রমাণ তত্ত্ব