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), पीपी। 983-1028। G.Japaridze, "कम्प्यूटेबिलिटी लॉजिक में सूत्रों से लेकर सर्केंट तक"। लॉजिकल मेथड्स इन कंप्यूटर साइंस 7 (2011), अंक 2, पेपर 1, पीपी। 1-55। G.Japaridze, "द टेमिंग ऑफ रिक्रेंसेस इन कम्प्यूटेबिलिटी लॉजिक थ्रू सर्केंट कैलकुलस, पार्ट I". आर्काइव फॉर मैथमेटिकल लॉजिक 52 (2013), पेज 173-212। G.Japaridze, "द टेमिंग ऑफ रिक्रेंसेस इन कम्प्यूटेबिलिटी लॉजिक थ्रू सर्केंट कैलकुलस, पार्ट II" आर्काइव फॉर मैथमेटिकल लॉजिक 52 (2013), पेज 213-259। आई. मेज़िरोव और एन. वेरेशचागिन, अमूर्त संसाधन शब्दार्थ और संगणनीयता तर्क पर। जर्नल ऑफ कंप्यूटर एंड सिस्टम साइंसेज 76 (2010), पृ. 356-372। डब्ल्यू. जू और S.Liu, "कम्प्यूटेबिलिटी लॉजिक के लिए सर्केंट कैलकुलस सिस्टम सीएल6 की मजबूती और पूर्णता"। लॉजिक जर्नल ऑफ द आई. जी. पी. एल. 20 (2012), पृ. 317-330। डब्ल्यू. जू और S.Liu, "प्रस्तावक तर्क के लिए संरचना प्रणाली एसकेएसजी के सर्केंट कलन प्रणाली सीएल8एस बनाम कलन"। मेंः मात्रात्मक तर्क और सॉफ्ट कम्प्यूटिंग। गुओजुन वांग, बिन झाओ और योंगमिंग ली, संस्करण। सिंगापुर, वर्ल्ड साइंटिफिक, 2012, पीपी। 144-149। डब्ल्यू. शू, "आई. एफ. तर्क के लिए जापारिद्ज़ के दृष्टिकोण से प्रेरित एक प्रस्तावात्मक प्रणाली"। लॉजिक जर्नल ऑफ द आई. जी. पी. एल. 22 (2014), पृष्ठ 982-991। डब्ल्यू. जू, क्लस्टरिंग और रैंकिंग के साथ एक सर्केंट कलन प्रणाली। जर्नल ऑफ एप्लाइड लॉजिक 16 (2016), पृ. 37-49। बाहरी लिंक तार्किक गणना प्रमाण सिद्धांत तार्किक अभिव्यक्तियाँ गैर-शास्त्रीय तर्क