Resolution proof compression by splitting
கணித தர்க்கத்தில், பிரிப்பதன் மூலம் ஆதார சுருக்கமானது ஒரு வழிமுறையாகும், இது தெளிவுத்திறன் சான்றுகளில் பிந்தைய செயல்முறையாக செயல்படுகிறது. ஸ்காட் காட்டன் தனது "தெளிவுத்திறன் ஆதாரத்தை குறைப்பதற்கான இரண்டு நுட்பங்கள்" என்ற கட்டுரையில் இதை முன்மொழிந்தார். பிளவு வழிமுறை பின்வரும் அவதானிப்பை அடிப்படையாகக் கொண்டதுஃ திருப்தியற்ற தன்மை மற்றும் மாறுபாட்டின் ஆதாரம் கொடுக்கப்பட்டால், ஆதாரத்தை மறுசீரமைப்பது (பிளவு) எளிதானது மற்றும் ஒரு ஆதாரம் மற்றும் இந்த இரண்டு சான்றுகளின் மறுசீரமைப்பு (கூடுதல் தெளிவுத்திறன் படி மூலம்) அசலை விட சிறிய ஆதாரத்தை விளைவிக்கலாம். ஒரு மாறியைப் பயன்படுத்தி ஒரு ஆதாரத்தில் பிளவுபடுவதைப் பயன்படுத்துவது வேறுபட்ட மாறியைப் பயன்படுத்தி வழிமுறையின் பிந்தைய பயன்பாட்டை செல்லாததாக்காது என்பதை நினைவில் கொள்க. உண்மையில், பருத்தி முன்மொழியப்பட்ட முறை சான்றுகளின் வரிசையை உருவாக்குகிறது, அங்கு ஒவ்வொரு ஆதாரமும் ஸ்ப்லிட்டிங்கைப் பயன்படுத்துவதன் விளைவாகும். வரிசையின் கட்டுமானத்தின் போது, ஒரு ஆதாரம் மிகப் பெரியதாக இருந்தால், அது மிகச்சிறிய ஆதாரமாக அமைக்கப்படுகிறது. ஒரு சிறந்த சுருக்க/நேர விகிதத்தை அடைய, மாறி தேர்வுக்கான ஒரு ஹூரிஸ்டிக் விரும்பத்தக்கது. இந்த நோக்கத்திற்காக, பருத்தி ஒரு தெளிவுத்திறன் படியின் "சேர்க்கை" யை வரையறுக்கிறது (முன்னோடிகள் மற்றும் தீர்க்கும் படிகளுடன்): பின்னர், ஒவ்வொரு மாறிக்கும், ஒரு மதிப்பெண் கணக்கிடப்படுகிறது, இது அனைத்து தெளிவுத்திறன் படிகளின் சேர்க்கையையும் இந்த தெளிவுத்திறன் படிகளின் எண்ணிக்கையுடன் இணைக்கிறது. இந்த வழியில் கணக்கிடப்பட்ட ஒவ்வொரு மதிப்பெண்ணையும் குறிக்கும் வகையில், ஒவ்வொரு மாறியும் அதன் மதிப்பெண்ணுக்கு விகிதாசாரமாக ஒரு நிகழ்தகவுடன் தேர்ந்தெடுக்கப்படுகிறதுஃ திருப்தியற்ற தன்மைக்கான ஆதாரத்தை ஒரு ஆதாரமாகவும் ஆதாரமாகவும் பிரிக்க, பருத்தி பின்வருவனவற்றை முன்மொழிகிறதுஃ ஒரு சொல்லர்த்தமானதைக் குறிக்கலாம் மற்றும் உட்பிரிவுகளின் தீர்வைக் குறிக்கலாம் மற்றும் எங்கே மற்றும் எங்கே. பின்னர், தெளிவுத்திறன் டேக்கில் உள்ள முனைகளில் வரைபடத்தை வரையறுக்கவும்ஃ மேலும், வெற்று உட்பிரிவாக இருக்கட்டும். பின்னர், மற்றும் முறையே கணக்கீடு மற்றும் மூலம் பெறப்படுகின்றன. குறிப்புகள் ஆதாரக் கோட்பாடு