Proof compression
પ્રૂફ થિયરીમાં, ગાણિતિક તર્કના ક્ષેત્રમાં, પ્રૂફ કમ્પ્રેશન એ ઔપચારિક સાબિતીઓને અલ્ગોરિધમિક રીતે સંકુચિત કરવાની સમસ્યા છે. વિકસિત અલ્ગોરિધમ્સનો ઉપયોગ SAT સોલ્વર્સ, એસએમટી-સોલ્વર્સ, ફર્સ્ટ-ઓર્ડર થીયરમ પ્રોવર્સ અને પ્રૂફ આસિસ્ટન્ટ્સ જેવા સ્વચાલિત થીયરમ પુરવાર કરનારા સાધનો દ્વારા પેદા થયેલા પુરાવાઓને સુધારવા માટે થઈ શકે છે. સમસ્યાનું પ્રતિનિધિત્વ પ્રપોઝિશનલ લોજિકમાં કલમ સી ના સમૂહમાંથી કલમનો રિઝોલ્યુશન પુરાવો એ નિર્દેશિત એસાયક્લિક ગ્રાફ (ડીએજી) છેઃ ઇનપુટ નોડ્સ એ સ્વયંસિદ્ધ તારણો છે (પરિસર વિના) જેના તારણો સી ના ઘટકો છે, રિઝોલ્વન્ટ નોડ્સ રિઝોલ્યુશન તારણો છે, અને સાબિતી નિષ્કર્ષ સાથે નોડ ધરાવે છે. ડી. એ. જી. એ નોડથી નોડ સુધીની ધાર ધરાવે છે જો અને માત્ર ત્યારે જ જો તેનો આધાર તારણ હોય. આ કિસ્સામાં, એક બાળક છે, અને તેના માતાપિતા છે. કોઈ બાળકો વિનાનું નોડ એ મૂળ છે. પ્રૂફ કમ્પ્રેશન અલ્ગોરિધમ ઓછા નોડ્સ સાથે નવું ડીએજી બનાવવાનો પ્રયાસ કરશે જે માન્ય સાબિતી રજૂ કરે છે અથવા, કેટલાક કિસ્સાઓમાં, તેના સબસેટના માન્ય સાબિતી રજૂ કરે છે. એક સરળ ઉદાહરણ ચાલો કલમોના સમૂહમાંથી કલમ માટે રિઝોલ્યુશન પ્રૂફ લઈએ અહીં આપણે જોઈ શકીએ છીએઃ અને ઇનપુટ નોડ્સ છે. નોડમાં એક ધરી હોય છે, ડાબી બાજુએ ઉકેલાયેલ શાબ્દિક જમણી બાજુએ ઉકેલાયેલ શાબ્દિક નિષ્કર્ષ એ છે કે કલમ પરિસર એ નોડ્સનો નિષ્કર્ષ છે અને (તેના માતાપિતા) ડીએજી હશે અને તેના માતાપિતા હશે અને તે સાબિતી એ (રીઝોલ્યુશન) નું મૂળ છે. સીનું ખંડન એ સીમાંના રિઝોલ્યુશન સાબિતી છે. તે એક સામાન્ય નોડ છે, જે કલમ અથવા કલમનો સંદર્ભ આપવા માટે છે જેનો અર્થ છે નિષ્કર્ષ કલમ, અને (પેટા) સાબિતી જેનો અર્થ છે (પેટા) સાબિતી જે તેના એકમાત્ર મૂળ તરીકે છે. કેટલાક કાર્યોમાં રિઝોલ્યુશન અનુમાનોની બીજગણિત રજૂઆત મળી શકે છે. પીવટ સાથે અને તેના રિઝોલ્વન્ટને આ રીતે સૂચવી શકાય છે. જ્યારે ધરી અનન્ય રીતે વ્યાખ્યાયિત અથવા અપ્રસ્તુત હોય છે, ત્યારે આપણે તેને અવગણીએ છીએ અને સરળ રીતે લખીએ છીએ. આ રીતે, કલમોના સમૂહને પરિવર્તનીય સંચાલક સાથે બીજગણિત તરીકે જોઈ શકાય છે; અને અનુરૂપ શબ્દ બીજગણિતની શરતો સંકેત શૈલીમાં ઠરાવ સાબિતીઓને સૂચવે છે જે સામાન્ય આલેખ સંકેત કરતાં ઠરાવ સાબિતીઓનું વર્ણન કરવા માટે વધુ સઘન અને વધુ અનુકૂળ હોય છે. આપણા છેલ્લા ઉદાહરણમાં ડી. એ. જી. નો સંકેત હશે અથવા ફક્ત આપણે ઓળખી શકીએ છીએ. સંકોચન અલ્ગોરિધમ્સ ક્રમિક કલન સાબિતીઓના સંકોચન માટેના અલ્ગોરિધમ્સમાં કટ પરિચય અને કટ નાબૂદીનો સમાવેશ થાય છે. પ્રપોઝિશનલ રિઝોલ્યુશન પ્રૂફના સંકોચન માટેના અલ્ગોરિધમ્સમાં રીસાયકલ યુનિટ્સ, રીસાયકલ પાઇવોટ્સ, રીસાયકલ પાઇવોટ્સ, ઇન્ટરસેક્શન, લોઅર યુનિટ્સ, લોઅર યુનિવલ્સ, સ્પ્લિટ, રિડ્યુસ એન્ડ રિકન્સ્ટ્રક્ટ અને સબઝમ્પશનનો સમાવેશ થાય છે. નોંધો પુરાવો સિદ્ધાંત