Resolution proof reduction via local context rewriting
প্রুফ থিওরি, গাণিতিক যুক্তির একটি ক্ষেত্র, স্থানীয় প্রসঙ্গ পুনর্লিখনের মাধ্যমে রেজোলিউশন প্রুফ হ্রাস স্থানীয় প্রসঙ্গ পুনর্লিখনের মাধ্যমে রেজোলিউশন প্রুফ হ্রাসের একটি কৌশল। এই প্রুফ কম্প্রেশন পদ্ধতিটি রিডিউস অ্যান্ড রিকনস্ট্রাকট নামে একটি অ্যালগরিদম হিসাবে উপস্থাপিত হয়েছিল, যা রেজোলিউশন প্রুফগুলির পোস্ট-প্রসেসিং হিসাবে কাজ করে। স্থানীয় প্রমাণ পুনর্লিখন নিয়মের একটি সেটের উপর ভিত্তি করে রিডিউস অ্যান্ড রিকনস্ট্রক্ট তৈরি করা হয় যা একটি সাবপ্রুফকে সমতুল্য বা শক্তিশালী হিসাবে রূপান্তরিত করে। প্রতিটি নিয়ম একটি নির্দিষ্ট প্রসঙ্গের সাথে মেলে সংজ্ঞায়িত করা হয়। একটি প্রসঙ্গে দুটি পিভট (এবং) এবং পাঁচটি ধারা (,, এবং) থাকে। একটি প্রসঙ্গের কাঠামো ()-এ দেখানো হয়েছে। লক্ষ্য করুন যে এটি বোঝায় যে এটি এবং (বিপরীত মেরুকরণ সহ) এবং এবং (বিপরীত মেরুকরণ সহ) রয়েছে। নীচের সারণিতে সিমোন ও অন্যান্যদের দ্বারা প্রস্তাবিত পুনর্লিখনের নিয়মগুলি দেখানো হয়েছে। অ্যালগরিদমের ধারণা হল এই নিয়মগুলি সুবিধাজনকভাবে প্রয়োগ করে প্রমাণের আকার হ্রাস করা। প্রথম পাঁচটি নিয়ম পূর্ববর্তী একটি গবেষণাপত্রে চালু করা হয়েছিল। উপরন্তুঃ নিয়ম এ 2 নিজে থেকে কোনও হ্রাস সম্পাদন করে না। যাইহোক, এটি এখনও কার্যকর, কারণ এর "অদলবদল" প্রভাব যা অন্যান্য নিয়ম প্রয়োগের জন্য নতুন সুযোগ তৈরি করতে পারে; নিয়ম এ1 অনুশীলনে ব্যবহার করা হয় না, কারণ এটি প্রমাণের আকার বাড়িয়ে দিতে পারে; নিয়ম বি1, বি2, বি2 'এবং বি3 হ্রাসের জন্য সরাসরি দায়ী, কারণ তারা মূলটির চেয়ে শক্তিশালী একটি রূপান্তরিত মূল ধারা তৈরি করে; বি নিয়মের প্রয়োগ একটি অবৈধ প্রমাণের দিকে নিয়ে যেতে পারে (নীচের উদাহরণটি দেখুন), কারণ রূপান্তরিত মূল ধারায় অনুপস্থিত কিছু আক্ষরিক শব্দগুলি প্রমাণের পথে অন্য রেজোলিউশন ধাপে জড়িত থাকতে পারে। অতএব, যখন এটি ঘটে তখন অ্যালগরিদমকেও একটি আইনি প্রমাণ "পুনর্গঠন" করতে হয়। নিম্নলিখিত উদাহরণটি এমন একটি পরিস্থিতি দেখায় যেখানে বি2 'নিয়ম প্রয়োগের পরে প্রমাণটি অবৈধ হয়ে যায়ঃ হাইলাইট করা প্রসঙ্গে নিয়ম বি2 প্রয়োগ করাঃ প্রমাণটি এখন অবৈধ কারণ রূপান্তরিত মূল ধারা থেকে আক্ষরিক অনুপস্থিত। প্রমাণটি পুনর্গঠনের জন্য, কেউ শেষ রেজোলিউশন ধাপের সাথে একসাথে অপসারণ করতে পারে (যা এখন অপ্রয়োজনীয়)। চূড়ান্ত ফলাফল হল নিম্নলিখিত আইনি (এবং শক্তিশালী) প্রমাণঃ 'বি2' নিয়ম প্রয়োগের একটি নতুন সুযোগ তৈরি করতে নিয়ম এ2 প্রয়োগ করে এই প্রমাণের আরও হ্রাস। সাধারণত এমন অনেক প্রসঙ্গ রয়েছে যেখানে নিয়ম এ2 প্রয়োগ করা যেতে পারে, তাই একটি সম্পূর্ণ পদ্ধতি সাধারণভাবে সম্ভব নয়। একটি প্রস্তাব হ 'ল দুটি সমাপ্তির মানদণ্ড সহ একটি লুপ হিসাবে রিডিউস অ্যান্ড রিকনস্ট্রক্ট কার্যকর করাঃ পুনরাবৃত্তির সংখ্যা এবং একটি সময়সীমা (যা প্রথমে পৌঁছেছে)। নীচের সিউডোকোডটি এটি দেখায়। 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 এর সাথে প্রতিস্থাপন করুন বা; 17 শেষ করুন 18 শেষ ফাংশনের জন্য যদি ইনপুট প্রমাণ একটি গাছ না হয় (সাধারণভাবে, রেজোলিউশন গ্রাফগুলি হয়) এই ক্ষেত্রে, পুনর্লিখন নিয়মের প্রয়োগ যাতে অন্যান্য সমাধানের পদক্ষেপে হস্তক্ষেপ না করে তা নিশ্চিত করার জন্য, একটি নিরাপদ সমাধান হল ধারা দ্বারা প্রতিনিধিত্ব করা নোডের একটি অনুলিপি তৈরি করা। এই সমাধানটি প্রমাণের আকার বাড়ায় এবং এটি করার সময় কিছু সতর্কতা প্রয়োজন। নিয়ম নির্বাচনের জন্য অনুসন্ধানমূলক একটি ভাল সংকোচন কর্মক্ষমতা অর্জনের জন্য গুরুত্বপূর্ণ। সিমোন ও অন্যান্য। নিয়মগুলির জন্য পছন্দের নিম্নলিখিত ক্রমটি ব্যবহার করুন (যদি প্রদত্ত প্রসঙ্গে প্রযোজ্য হয়): বি2> বি3> {বি2 ', বি1}> এ1'> এ2 (এক্স> ওয়াই মানে এক্সকে ওয়াই-এর চেয়ে বেশি পছন্দ করা হয়)। পরীক্ষাগুলি দেখিয়েছে যে শুধুমাত্র রিডিউস অ্যান্ড রিকনস্ট্রাকটের কম্প্রেশন/সময়ের অনুপাত অ্যালগরিদম রিসাইক্লপিভটসের তুলনায় খারাপ। যাইহোক, রিসাইকলপিভটস শুধুমাত্র একটি প্রমাণের জন্য একবার প্রয়োগ করা যেতে পারে, তবে আরও ভাল সংকোচন তৈরি করতে রিডিউস অ্যান্ড রিকনস্ট্রক্ট একাধিকবার প্রয়োগ করা যেতে পারে। রিডিউস অ্যান্ড রিকনস্ট্রক্ট এবং রিসাইকলপিভটস অ্যালগরিদমগুলিকে একত্রিত করার প্রচেষ্টা ভাল ফলাফলের দিকে পরিচালিত করেছে। সিউডোকোড প্রমাণ তত্ত্বের উদাহরণ সহ নিবন্ধগুলি নোট করুন