Resolution proof reduction via local context rewriting
પ્રૂફ થિયરીમાં, ગાણિતિક તર્કનું ક્ષેત્ર, સ્થાનિક સંદર્ભ પુનર્લેખન દ્વારા રિઝોલ્યુશન પ્રૂફ રિડક્શન એ સ્થાનિક સંદર્ભ પુનર્લેખન દ્વારા રિઝોલ્યુશન પ્રૂફ રિડક્શન માટેની તકનીક છે. આ પ્રૂફ કમ્પ્રેશન પદ્ધતિને રિડ્યુસ એન્ડ રિકન્સ્ટ્રક્ટ નામના અલ્ગોરિધમ તરીકે રજૂ કરવામાં આવી હતી, જે રિઝોલ્યુશન પ્રૂફની પોસ્ટ-પ્રોસેસિંગ તરીકે કામ કરે છે. રિડ્યૂસ એન્ડ રિકન્સ્ટ્રક્ટ એ સ્થાનિક પ્રૂફ રીરાઇટિંગ નિયમોના સમૂહ પર આધારિત છે જે સબપ્રૂફને સમકક્ષ અથવા મજબૂતમાં રૂપાંતરિત કરે છે. દરેક નિયમને ચોક્કસ સંદર્ભ સાથે મેળ કરવા માટે વ્યાખ્યાયિત કરવામાં આવે છે. સંદર્ભમાં બે ધરીઓ (અને) અને પાંચ કલમો (,,, અને) નો સમાવેશ થાય છે. સંદર્ભની રચના () માં દર્શાવવામાં આવી છે. નોંધ લો કે આ સૂચવે છે કે તે અને (વિરુદ્ધ ધ્રુવીયતા સાથે) માં સમાયેલ છે અને અને (વિરુદ્ધ ધ્રુવીયતા સાથે પણ) માં સમાયેલ છે. નીચેનું કોષ્ટક સિમોન એટ અલ દ્વારા પ્રસ્તાવિત પુનર્લેખનના નિયમો દર્શાવે છે. અલ્ગોરિધમનો વિચાર આ નિયમોને તકવાદી રીતે લાગુ કરીને સાબિતીનું કદ ઘટાડવાનો છે. પ્રથમ પાંચ નિયમો અગાઉના પેપરમાં રજૂ કરવામાં આવ્યા હતા. વધુમાંઃ નિયમ A2 તેના પોતાના પર કોઈ ઘટાડો કરતું નથી. જો કે, તે હજુ પણ ઉપયોગી છે, કારણ કે તેની "ફેરબદલ" અસર અન્ય નિયમોને લાગુ કરવા માટે નવી તકો ઊભી કરી શકે છે; વ્યવહારમાં નિયમ A1 નો ઉપયોગ થતો નથી, કારણ કે તે સાબિતીના કદમાં વધારો કરી શકે છે; નિયમો B1, B2, B2 'અને B3 ઘટાડા માટે સીધા જવાબદાર છે, કારણ કે તેઓ મૂળ કરતાં વધુ મજબૂત રૂપાંતરિત મૂળ કલમ ઉત્પન્ન કરે છે; B નિયમનો ઉપયોગ ગેરકાયદેસર સાબિતી તરફ દોરી શકે છે (નીચેનું ઉદાહરણ જુઓ), કારણ કે રૂપાંતરિત મૂળ કલમમાં ગુમ થયેલ કેટલાક અક્ષરો સાબિતીના માર્ગ સાથે બીજા ઠરાવ પગલામાં સામેલ હોઈ શકે છે. તેથી, જ્યારે આવું થાય ત્યારે એલ્ગોરિધમે કાનૂની સાબિતીનું "પુનર્નિર્માણ" પણ કરવું પડે છે. નીચેનું ઉદાહરણ એવી પરિસ્થિતિ દર્શાવે છે કે જ્યાં B2 'નિયમ લાગુ થયા પછી સાબિતી ગેરકાયદેસર બની જાય છેઃ હાઇલાઇટ કરેલા સંદર્ભમાં નિયમ B2 લાગુ કરવોઃ સાબિતી હવે ગેરકાયદેસર છે કારણ કે રૂપાંતરિત મૂળ કલમમાંથી શાબ્દિક ખૂટે છે. સાબિતીનું પુનઃનિર્માણ કરવા માટે, છેલ્લા રિઝોલ્યુશન પગલા (જે હવે બિનજરૂરી છે) સાથે એકસાથે દૂર કરી શકાય છે. અંતિમ પરિણામ નીચેનો કાનૂની (અને મજબૂત) પુરાવો છેઃ નિયમ B2 'લાગુ કરવાની નવી તક ઊભી કરવા માટે નિયમ A2 લાગુ કરીને આ પુરાવોમાં વધુ ઘટાડો. સામાન્ય રીતે એવા ઘણા સંદર્ભો હોય છે જ્યાં નિયમ A2 લાગુ થઈ શકે છે, તેથી એક સંપૂર્ણ અભિગમ સામાન્ય રીતે શક્ય નથી. એક દરખાસ્ત એ છે કે રિડ્યુસ એન્ડ રિકન્સ્ટ્રક્ટને બે સમાપ્તિ માપદંડ સાથે લૂપ તરીકે અમલમાં મૂકવુંઃ પુનરાવર્તનની સંખ્યા અને સમયસમાપ્તિ (જે પહેલા પહોંચી શકાય છે). નીચેનો સ્યુડોકોડ આ દર્શાવે છે. 1 વિધેય ReduceAndReconstruct (/* a પ્રૂફ */, ટાઇમલિમિટ, મેક્સિમઇટરેશન્સ): i = 1 માટે 2 થી મહત્તમઇટરેશન્સ કરો 3 ReduceAndReconstructLoop (); 4 જો સમય> ટાઇમલિમિટ હોય તો// ટાઇમઆઉટ 5 વિરામ; 7 અંતિમ કાર્ય માટે 6 અંત ReduceAndReconstruct એ ReduceAndReconstructLoop કાર્યનો ઉપયોગ કરે છે, જે નીચે સ્પષ્ટ થયેલ છે. અલ્ગોરિધમનો પ્રથમ ભાગ રિઝોલ્યુશન ગ્રાફનો ટોપોલોજિકલ ક્રમ કરે છે (ધાર પૂર્વવર્તીઓથી રિઝોલ્વન્ટ્સ સુધી જાય છે તે ધ્યાનમાં રાખીને). આ સુનિશ્ચિત કરવા માટે કરવામાં આવે છે કે દરેક નોડની મુલાકાત તેના પૂર્વજો પછી લેવામાં આવે (આ રીતે, તૂટેલા રીઝોલ્યુશન પગલાં હંમેશા મળી આવે છે અને નિશ્ચિત થાય છે). 1 વિધેય રિડ્યુસ એન્ડ રિકન્સ્ટ્રક્ટ લૂપ (/* એક પુરાવો */): 2 ટી. એસ. = ટોપોલોજિકલ સોર્ટિંગ (); ટી. એસ. 4 માં દરેક નોડ માટે 3 જો લીફ 5 ન હોય તો અને પછી 6 = રિઝોલ્યુશન (,); 7 નો ડાબો સંદર્ભ નક્કી કરો, જો કોઈ હોય તો; 8 નો સાચો સંદર્ભ નક્કી કરો, જો કોઈ હોય તો; 9 સંશોધનાત્મક રીતે એક સંદર્ભ પસંદ કરો (જો કોઈ હોય તો) અને અનુરૂપ નિયમ લાગુ કરો; 10 અન્ય જો અને પછી 11 સાથે બદલો; 12 અન્ય જો અને પછી 13 સાથે બદલો; 14 અન્ય જો અને પછી 15 સંશોધનાત્મક રીતે પૂર્વવર્તી પસંદ કરો અથવા; 16 સાથે અથવા સાથે બદલો; 18 અંતિમ કાર્ય માટે 17 અંત જો ઇનપુટ પ્રૂફ વૃક્ષ નથી (સામાન્ય રીતે, રીઝોલ્યુશન ગ્રાફ છે) આ કિસ્સામાં, પુનર્લેખન નિયમની અરજી અન્ય ઠરાવ પગલાંઓમાં દખલ નહીં કરે તેની ખાતરી કરવા માટે, કલમ દ્વારા રજૂ કરાયેલા નોડની નકલ બનાવવી એ સલામત ઉકેલ છે. આ દ્રાવણ સાબિતીના કદમાં વધારો કરે છે અને આમ કરતી વખતે થોડી સાવધાની રાખવાની જરૂર છે. સારા સંકોચન પ્રદર્શનને પ્રાપ્ત કરવા માટે નિયમ પસંદગી માટે સંશોધનાત્મક મહત્વપૂર્ણ છે. સિમોન એટ અલ. નિયમો માટે પસંદગીના નીચેના ક્રમનો ઉપયોગ કરો (જો આપેલ સંદર્ભમાં લાગુ પડે તો): B2> B3> {B2 ', B1}> A1'> A2 (X> Y નો અર્થ છે કે X ને Y કરતા વધુ પસંદ કરવામાં આવે છે). પ્રયોગોએ દર્શાવ્યું છે કે એકલા રિડ્યુસ એન્ડ રિકન્સ્ટ્રક્ટમાં અલ્ગોરિધમ રીસાયકલ પાઇવોટ્સ કરતાં વધુ ખરાબ સંકોચન/સમય ગુણોત્તર છે. જો કે, જ્યારે રીસાયકલ પાઇવોટ્સને સાબિતી પર માત્ર એક જ વાર લાગુ કરી શકાય છે, ત્યારે વધુ સારું સંકોચન ઉત્પન્ન કરવા માટે રિડ્યુસ એન્ડ રિકન્સ્ટ્રક્ટને ઘણી વખત લાગુ કરી શકાય છે. રિડ્યુસ એન્ડ રિકન્સ્ટ્રક્ટ અને રીસાયકલ પાઇવોટ્સ અલ્ગોરિધમ્સને જોડવાના પ્રયાસથી સારા પરિણામો મળ્યા છે. સ્યુડોકોડ પ્રૂફ થિયરીના ઉદાહરણો સાથેના લેખો નોંધે છે