Cirquent calculus
સર્ક્યુઅન્ટ કેલ્ક્યુલસ એ એક પ્રૂફ કેલ્ક્યુલસ છે જે ફોર્મ્યુલા અથવા સિક્વેન્ટ્સ જેવી પરંપરાગત વૃક્ષ-શૈલીની વસ્તુઓના વિરોધમાં, સર્ક્યુઅન્ટ્સ તરીકે ઓળખાતી ગ્રાફ-શૈલીની રચનાઓમાં હેરફેર કરે છે. સર્ક્યુન્ટ્સ વિવિધ સ્વરૂપોમાં આવે છે, પરંતુ તે બધા એક મુખ્ય લાક્ષણિકતા ધરાવે છે, જે તેમને વાક્યરચના હેરફેરના વધુ પરંપરાગત પદાર્થોથી અલગ બનાવે છે. આ લક્ષણ એ વિવિધ ઘટકો વચ્ચે પેટા ઘટકોની સંભવિત વહેંચણી માટે સ્પષ્ટપણે જવાબદાર હોવાની ક્ષમતા છે. દાખલા તરીકે, એવી અભિવ્યક્તિ લખવી શક્ય છે કે જ્યાં બે પેટા અભિવ્યક્તિઓ F અને E હોય, જ્યારે એક પણ બીજાની પેટા અભિવ્યક્તિ ન હોય, ત્યારે પણ પેટા અભિવ્યક્તિ G ની સામાન્ય ઘટના હોય (G ની બે જુદી જુદી ઘટનાઓ હોવાના વિરોધમાં, એક F માં અને એક E માં). ઝાંખી આ અભિગમ જી. જાપારિડ્ઝે દ્વારા વૈકલ્પિક સાબિતી સિદ્ધાંત તરીકે રજૂ કરવામાં આવ્યો હતો, જે તેમના ગણતરીક્ષમતા તર્કના વિવિધ બિન-તુચ્છ ટુકડાઓને "કાબૂમાં" રાખવા માટે સક્ષમ હતો, જેણે અન્યથા પરંપરાગત સાબિતી-સૈદ્ધાંતિક માળખામાં તમામ સ્વયંસિદ્ધીકરણ પ્રયાસોનો વિરોધ કર્યો હતો. "સર્ક્યુઅન્ટ" શબ્દની ઉત્પત્તિ સિર્ક્યુઅન્ટ + સિક્યુઅન્ટ છે, જે સર્ક્યુઅન્ટનું સૌથી સરળ સ્વરૂપ છે, જ્યારે સૂત્રોને બદલે સર્કિટ જેવું લાગે છે, તેને એકતરફી સિક્વન્ટના સંગ્રહ તરીકે વિચારી શકાય છે (દાખલા તરીકે, જેન્ટ્ઝેન-શૈલીના પ્રૂફ ટ્રીના આપેલ સ્તરની સિક્વન્ટ) જ્યાં કેટલાક સિક્વન્ટમાં વહેંચાયેલ તત્વો હોઈ શકે છે. સર્ક્યુન્ટ કલનનું મૂળભૂત સંસ્કરણ "અમૂર્ત સંસાધન શબ્દાર્થ" સાથે હતું અને દાવો કરવામાં આવ્યો હતો કે બાદમાં પરંપરાગત રીતે રેખીય તર્ક સાથે સંકળાયેલ સંસાધન ફિલસૂફીનું પર્યાપ્ત ઔપચારિકરણ હતું. તે દાવા અને સિમેન્ટિક્સે (સંલગ્ન) રેખીય તર્ક કરતાં યોગ્ય રીતે મજબૂત તર્કને પ્રેરિત કર્યો તે હકીકતના આધારે, જાપારિડ્ઝે દલીલ કરી હતી કે સંસાધનોના તર્ક તરીકે રેખીય તર્ક અપૂર્ણ છે. વધુમાં, તેમણે એવી દલીલ કરી હતી કે માત્ર અનુમાનાત્મક શક્તિ જ નહીં પરંતુ રેખીય તર્કની અભિવ્યક્ત શક્તિ પણ નબળી હતી, કારણ કે તે, સર્ક્યુઅન્ટ કલનથી વિપરીત, સંસાધન વહેંચણીની સર્વવ્યાપક ઘટનાને પકડવામાં નિષ્ફળ રહી હતી. સર્ક્યુન્ટ કલનની સંસાધન ફિલસૂફી રેખીય તર્ક અને શાસ્ત્રીય તર્કના અભિગમોને બે ચરમસીમાઓ તરીકે જુએ છેઃ પહેલું કોઈપણ વહેંચણીને બિલકુલ મંજૂરી આપતું નથી, જ્યારે પછીનું "બધું વહેંચાયેલું છે જે વહેંચી શકાય છે". સર્ક્યુઅન્ટ કેલ્ક્યુલસથી વિપરીત, કોઈ પણ અભિગમ મિશ્રિત કેસોને મંજૂરી આપતો નથી જ્યાં કેટલાક સમાન પેટા સૂત્રો વહેંચવામાં આવે છે અને કેટલાક નથી. સર્ક્યુઅન્ટ કલનની પાછળથી મળી આવેલી એપ્લિકેશનોમાં તેનો ઉપયોગ શુદ્ધ પ્રસ્તાવાત્મક સ્વતંત્રતા-મૈત્રીપૂર્ણ તર્ક માટે શબ્દાર્થને વ્યાખ્યાયિત કરવા માટે કરવામાં આવ્યો હતો. અનુરૂપ તર્કને ડબ્લ્યુ. ઝુ દ્વારા સ્વયંસિદ્ધ કરવામાં આવ્યો હતો. સિન્ટેક્ટિકલી રીતે, સર્ક્યુઅન્ટ કેલ્ક્યુલી એ સબફોર્મ્યુલા-શેરિંગના અનન્ય લક્ષણ સાથે ઊંડી અનુમાન પ્રણાલીઓ છે. આ સુવિધા ચોક્કસ પુરાવાઓ માટે ઝડપ પૂરી પાડતી હોવાનું દર્શાવવામાં આવ્યું છે. દાખલા તરીકે, પ્રસ્તાવિત કબૂતરોના છિદ્ર માટે બહુપદી કદના વિશ્લેષણાત્મક પુરાવાઓનું નિર્માણ કરવામાં આવ્યું છે. અન્ય ઊંડા અનુમાન પ્રણાલીઓમાં આ સિદ્ધાંત માટે માત્ર અર્ધ-બહુપદી વિશ્લેષણાત્મક પુરાવાઓ મળી આવ્યા છે. રિઝોલ્યુશન અથવા વિશ્લેષણાત્મક જેન્ટ્ઝેન-શૈલી પ્રણાલીઓમાં, કબૂતર છિદ્ર સિદ્ધાંતમાં માત્ર ઘાતાંકીય કદના પુરાવા હોવાનું જાણીતું છે. સંદર્ભ સાહિત્ય M.Bauer, "પ્રપોઝિશનલ સર્ક્યુન્ટ કેલ્ક્યુલસની કોમ્પ્યુટેશનલ જટિલતા". કોમ્પ્યુટર સાયન્સમાં લોજિકલ મેથડ્સ 11 (2015), અંક 1, પેપર 12, પીપી. 1-16. G.Japaridze, "સર્ક્યુન્ટ કેલ્ક્યુલસ અને એબ્સ્ટ્રેક્ટ રિસોર્સ સિમેન્ટિક્સનો પરિચય". જર્નલ ઓફ લોજિક એન્ડ કમ્પ્યુટેશન 16 (2006), પૃ. 489-532. G.Japaridze, "સર્ક્યુન્ટ કેલ્ક્યુલસ ડીપેન્ડ". જર્નલ ઓફ લોજિક એન્ડ કમ્પ્યુટેશન 18 (2008), pp. 983-1028. G.Japaridze, "ફોર્મ્યુલાઓથી માંડીને કોમ્પ્યુટેબિલિટી લોજિકમાં સર્ક્યુન્ટ્સ સુધી". કોમ્પ્યુટર સાયન્સમાં લોજિકલ મેથડ્સ 7 (2011), અંક 2, પેપર 1, પીપી. 1-55. G.Japaridze, "ધ ટેમિંગ ઓફ રિક્રન્સિસ ઇન કમ્પ્યુટેબિલિટી લોજિક થ્રુ સર્ક્યુન્ટ કેલ્ક્યુલસ, પાર્ટ I". આર્કાઇવ ફોર મેથેમેટિકલ લોજિક 52 (2013), પૃષ્ઠો 173-212. G.Japaridze, "ધ ટેમિંગ ઓફ રિક્રન્સિસ ઇન કમ્પ્યુટેબિલિટી લોજિક થ્રુ સર્ક્યુન્ટ કેલ્ક્યુલસ, પાર્ટ II" આર્કાઇવ ફોર મેથેમેટિકલ લોજિક 52 (2013), પૃષ્ઠો 213-259. I. મેઝિરોવ અને N. વેરેશચાગિન, અમૂર્ત સંસાધન શબ્દાર્થ અને ગણતરીક્ષમતા તર્ક પર. જર્નલ ઓફ કમ્પ્યુટર એન્ડ સિસ્ટમ સાયન્સિસ 76 (2010), પૃષ્ઠ. 356-372. W. Xu અને S.Liu, "કોમ્પ્યુટેબિલિટી લોજિક માટે સર્ક્યુઅન્ટ કેલ્ક્યુલસ સિસ્ટમ CL6 ની મજબૂતી અને સંપૂર્ણતા". લોજિક જર્નલ ઓફ ધ આઇ. જી. પી. એલ. 20 (2012), પૃ. 317-330. W. Xu અને S.Liu, "પ્રપોઝિશનલ લોજિક માટે સર્ક્વન્ટ કેલ્ક્યુલસ સિસ્ટમ CL8S વિરુદ્ધ સ્ટ્રક્ચર્સ સિસ્ટમ SKSgનું કેલ્ક્યુલસ". માંઃ ક્વોન્ટિટેટિવ લોજિક અને સોફ્ટ કમ્પ્યુટિંગ. ગુઓજુન વાંગ, બિન ઝાઓ અને યોંગમિંગ લી, આવૃત્તિઓ. સિંગાપોર, વર્લ્ડ સાયન્ટિફિક, 2012, પીપી. 144-149. ડબલ્યુ. ઝુ, "આઇએફ તર્ક પ્રત્યે જાપારિડેઝના અભિગમ દ્વારા પ્રેરિત એક પ્રસ્તાવાત્મક પ્રણાલી". લોજિક જર્નલ ઓફ ધ આઇ. જી. પી. એલ. 22 (2014), પૃષ્ઠો 982-991. ડબલ્યુ. ઝુ, ક્લસ્ટરિંગ અને રેન્કિંગ સાથેની એક સર્ક્યુઅન્ટ કલન પદ્ધતિ. જર્નલ ઓફ એપ્લાઇડ લોજિક 16 (2016), પૃષ્ઠ. 37-49. બાહ્ય કડીઓ તાર્કિક ગણતરી પુરાવો સિદ્ધાંત તાર્કિક અભિવ્યક્તિઓ બિન-શાસ્ત્રીય તર્ક