Proof compression
ஆதாரக் கோட்பாட்டில், கணித தர்க்கத்தின் ஒரு பகுதி, ஆதார சுருக்கமானது முறையான ஆதாரங்களை வழிமுறை ரீதியாக சுருக்குவதில் உள்ள சிக்கலாகும். எஸ்ஏடி தீர்வுகள், எஸ்எம்டி-தீர்வுகள், முதல்-வரிசை தேற்றம் நிரூபகங்கள் மற்றும் ஆதார உதவியாளர்கள் போன்ற தானியங்கி தேற்றத்தை நிரூபிக்கும் கருவிகளால் உருவாக்கப்படும் ஆதாரங்களை மேம்படுத்த உருவாக்கப்பட்ட வழிமுறைகளைப் பயன்படுத்தலாம். சிக்கல் பிரதிநிதித்துவம் முன்மொழிவு தர்க்கத்தில் C உட்பிரிவுகளின் தொகுப்பிலிருந்து ஒரு பிரிவின் தெளிவுத்திறன் சான்று ஒரு இயக்கப்படும் அசைக்ளிக் கிராஃப் (டிஏஜி) ஆகும்ஃ உள்ளீட்டு முனைகள் என்பது தன்னியக்க அனுமானங்கள் (வளாகம் இல்லாமல்), அவற்றின் முடிவுகள் சி இன் கூறுகள், தீர்க்கும் முனைகள் தெளிவுத்திறன் அனுமானங்கள், மற்றும் ஆதாரம் முடிவுடன் ஒரு முனையைக் கொண்டுள்ளது. டிஏஜி ஒரு முனையிலிருந்து ஒரு முனைக்கு ஒரு விளிம்பைக் கொண்டுள்ளது, அதன் ஒரு முன்மாதிரி முடிவாக இருந்தால் மட்டுமே. இந்த வழக்கில், ஒரு குழந்தை, மற்றும் ஒரு பெற்றோர். குழந்தைகள் இல்லாத ஒரு முனை ஒரு வேர். ஒரு ஆதார சுருக்க வழிமுறை குறைவான முனைகளைக் கொண்ட ஒரு புதிய டிஏஜியை உருவாக்க முயற்சிக்கும், இது ஒரு செல்லுபடியாகும் ஆதாரத்தைக் குறிக்கிறது அல்லது சில சந்தர்ப்பங்களில், ஒரு துணைக்குழுவின் செல்லுபடியாகும் ஆதாரத்தைக் குறிக்கிறது. ஒரு எளிய எடுத்துக்காட்டு, உட்பிரிவுகளின் தொகுப்பிலிருந்து உட்பிரிவுக்கான தெளிவுத்திறன் ஆதாரத்தை எடுத்துக்கொள்வோம் இங்கே நாம் காணலாம்ஃ மற்றும் உள்ளீட்டு முனைகள். முனை ஒரு மையத்தைக் கொண்டுள்ளது, இடது தீர்க்கப்பட்ட நேரடி தீர்க்கப்பட்ட நேரடி முடிவு என்பது பிரிவு வளாகங்கள் முனைகளின் முடிவு மற்றும் (அதன் பெற்றோர்) டிஏஜி ஒரு குழந்தை மற்றும் ஆதாரத்தின் மூலமாகும் A (தீர்மானம்) மறுப்பு C இன் மறுப்பு என்பது C இலிருந்து ஒரு தீர்மான ஆதாரமாகும். இது ஒரு பொதுவான கொடுக்கப்பட்ட முனையாகும், இது உட்பிரிவு அல்லது உட்பிரிவைக் குறிக்கிறது, அதாவது முடிவு உட்பிரிவு, மற்றும் (துணை) ஆதாரம் என்பது (துணை) ஆதாரத்தை அதன் ஒரே மூலமாகக் கொண்டுள்ளது. சில படைப்புகளில் தெளிவுத்திறன் அனுமானங்களின் இயற்கணித பிரதிநிதித்துவத்தைக் காணலாம். இன் மற்றும் பிவோட் கொண்ட ரிசல்வன்ட்டை இவ்வாறு குறிக்கலாம். மையப்பகுதி தனித்துவமாக வரையறுக்கப்படும்போது அல்லது பொருத்தமற்றதாக இருக்கும்போது, நாம் அதைத் தவிர்த்து வெறுமனே எழுதுகிறோம். இந்த வழியில், உட்பிரிவுகளின் தொகுப்பை ஒரு பரிமாற்ற ஆபரேட்டருடன் கூடிய இயற்கணிதமாகக் காணலாம்; மேலும் அதனுடன் தொடர்புடைய சொல் இயற்கணிதத்தில் உள்ள சொற்கள் ஒரு குறியீட்டு பாணியில் தெளிவுத்திறன் சான்றுகளைக் குறிக்கின்றன, இது வழக்கமான வரைபடக் குறியீட்டை விட தெளிவுத்திறன் சான்றுகளை விவரிக்க மிகவும் கச்சிதமாகவும் வசதியாகவும் இருக்கும். நமது கடைசி எடுத்துக்காட்டில் DAG இன் குறியீடு அல்லது வெறுமனே நாம் அடையாளம் காண முடியும். சுருக்க வழிமுறைகள் தொடர்ச்சியான கால்குலஸ் சான்றுகளின் சுருக்கத்திற்கான வழிமுறைகளில் வெட்டு அறிமுகம் மற்றும் வெட்டு நீக்குதல் ஆகியவை அடங்கும். முன்மொழிவு தெளிவுத்திறன் சான்றுகளின் சுருக்கத்திற்கான வழிமுறைகளில் மறுசுழற்சி அலகுகள், மறுசுழற்சி மையங்கள், மறுசுழற்சி மையங்கள், கீழ் மையங்கள், கீழ் மையங்கள், பிளவு, குறைத்தல் மற்றும் மறுசீரமைப்பு மற்றும் உட்பிரிவு ஆகியவை அடங்கும். குறிப்புகள் ஆதாரக் கோட்பாடு