रेखीय तर्क

रैखिक तर्क जीन-यवेस गिरार्ड द्वारा चिरसम्मत और अंतर्ज्ञानवादी तर्क के परिशोधन के रूप में प्रस्तावित एक उप-संरचनात्मक तर्क है, जो बाद के कई रचनात्मक गुणों के साथ पूर्व के द्वंद्वों को जोड़ता है।^[1] हालाँकि तर्क का अध्ययन अपने स्वयं के लिए भी किया गया है, अधिक व्यापक रूप से, रैखिक तर्क के विचार प्रोग्रामिंग भाषाओं, गेम शब्दार्थ और क्वांटम भौतिकी (क्योंकि रैखिक तर्क को क्वांटम सूचना सिद्धांत के तर्क के रूप में देखा जा सकता है),^[2] और साथ ही भाषाविज्ञान,^[3] विशेष रूप से संसाधन-सीमा, द्वैत और सहभागिता जैसे क्षेत्रों में प्रभावशाली रहे हैं।

रेखीय तर्क कई अलग-अलग प्रस्तुतियों, स्पष्टीकरण और अंतर्ज्ञान के लिए उत्तरदायी है। प्रमाण-सैद्धांतिक रूप से, यह चिरसम्मत अनुक्रम कैलकुलस के विश्लेषण से निकला है जिसमें (संरचनात्मक नियमों) संकुचन और कमजोर पड़ने के उपयोग को सावधानीपूर्वक नियंत्रित किया जाता है। परिचालनात्मक रूप से, इसका मतलब यह है कि तार्किक कटौती अब लगातार "सच्चाई" के लगातार बढ़ते संग्रह के बारे में नहीं है, बल्कि संसाधनों में हेरफेर करने का एक तरीका भी है जिसे हमेशा दोहराया नहीं जा सकता है या इच्छानुसार फेंक नहीं दिया जा सकता है। सरल सांकेतिक मॉडल के संदर्भ में, रैखिक तर्क को कार्टेशियन (बंद) श्रेणियों को सममित मोनोइडल (बंद) श्रेणियों के साथ प्रतिस्थापित करके अंतर्ज्ञानवादी तर्क की व्याख्या को परिष्कृत करने के रूप में देखा जा सकता है, या बूलियन बीजगणित को C*-बीजगणित के साथ प्रतिस्थापित करके चिरसम्मत तर्क की व्याख्या के रूप में देखा जा सकता है।

संयोजकता, द्वंद्व, और ध्रुवता

सिंटेक्स

चिरसम्मत रैखिक तर्क (सीएलएल) की भाषा को बीएनएफ नोटेशन द्वारा आगमनात्मक रूप से परिभाषित किया गया है।

$A$	::=	$p ∣ p ⊥$
	$∣$	$A \otimes A ∣ A \oplus A$
	$∣$	$A & A ∣ A ⅋ A$
	$∣$	$1 ∣ 0 ∣ ⊤ ∣ ⊥$
	$∣$	$! A ∣ ? A$

यहां $p$ और $p ⊥$ का दायरा तार्किक परमाणुओं से अधिक है। नीचे बताए जाने वाले कारणों के लिए, संयोजक ⊗, ⅋, 1, और ⊥ को गुणक कहा जाता है, संयोजक &, ⊕, ⊤, और 0 को योगज कहा जाता है, और संयोजक ! और ? घातांक कहा जाता है. हम निम्नलिखित शब्दावली को आगे भी नियोजित कर सकते हैं:


प्रतीक	नाम
⊗	गुणक संयोजन	टाइम्स	टेन्सर
⊕	योगात्मक विच्छेदन	प्लस
&	योगात्मक संयोजन	साथ
⅋	गुणन विच्छेद	पार
!	अवश्य	बैंग
?	क्यों नहीं

बाइनरी संयोजक ⊗, ⊕, & और ⅋ साहचर्य और क्रमविनिमेय हैं; 1 ⊗ की इकाई है, 0 ⊕ की इकाई है, ⊥ ⅋ की इकाई है और ⊤ & की इकाई है।

प्रत्येक प्रस्ताव $A$ सीएलएल में दोहरा $A ⊥$ है, इस प्रकार परिभाषित:

$(p) ⊥ = p ⊥$			$(p ⊥) ⊥ = p$
$(A \otimes B) ⊥ = A ⊥ ⅋ B ⊥$			$(A ⅋ B) ⊥ = A ⊥ \otimes B ⊥$
$(A \oplus B) ⊥ = A ⊥ & B ⊥$			$(A & B) ⊥ = A ⊥ \oplus B ⊥$
$(1) ⊥ = ⊥$			$(⊥) ⊥ = 1$
$(0) ⊥ = ⊤$			$(⊤) ⊥ = 0$
$(! A) ⊥ = ?(A ⊥)$			$(? A) ⊥ = !(A ⊥)$

संयोजकों का वर्गीकरण
	योग	गुणन	ईएक्सपी
धनात्मक	⊕ 0	⊗ 1	!
ऋणत्मक	& ⊤	⅋ ⊥	?

ध्यान दें कि $(-) ⊥$ एक समावेश है, यानी, सभी प्रस्तावों के लिए $A ⊥⊥ = A$ $A ⊥$ को $A$ का रैखिक निषेधन भी कहा जाता है।

तालिका के कॉलम रैखिक तर्क के संयोजकों को वर्गीकृत करने का एक और तरीका सुझाते हैं, जिसे ध्रुवीयता कहा जाता है: बाएं कॉलम में संयोजक ऋणात्मक हैं (⊗, ⊕, 1, 0, !) को धनात्मक कहा जाता है, जबकि दाहिनी ओर उनके दोहरे (⅋, &, ⊥, ⊤, ?) को ऋणात्मक कहा जाता है; दाहिनी ओर cf तालिका।

संयोजकों के व्याकरण में रैखिक निहितार्थ शामिल नहीं है, लेकिन $A ⊸ B := A ⊥ ⅋ B$ द्वारा रैखिक निषेध और गुणक विच्छेदन का उपयोग करके सीएलएल में निश्चित किया जा सकता है। संयोजक ⊸ को कभी-कभी इसके आकार के कारण "लॉलीपॉप" कहा जाता है।

अनुक्रमिक कलन प्रस्तुति

रैखिक तर्क को परिभाषित करने का एक तरीका अनुक्रमिक कलन के रूप में है। हम प्रस्तावों $A 1, ..., A n$ जिन्हें संदर्भ भी कहा जाता है, की सूची को विस्तृत करने के लिए $Γ$ और $Δ$ अक्षरों का उपयोग करते हैं। एक अनुक्रम टर्नस्टाइल के बाएँ और दाएँ पर एक संदर्भ रखता है, जिसे $\vdash$ लिखा जाता है। सहज रूप से, अनुक्रम इस बात पर जोर देता है कि $Γ$ का संयोजन $Δ$ के विच्छेदन पर जोर देता है (हालांकि हमारा मतलब "गुणक" संयोजन और विच्छेदन है, जैसा कि नीचे बताया गया है)। गिरार्ड केवल एक तरफा अनुक्रमों (जहां बाएं हाथ का संदर्भ खाली है) का उपयोग करके चिरसम्मत रैखिक तर्क का वर्णन करता है, और हम यहां उस अधिक किफायती प्रस्तुति का पालन करते हैं। यह संभव है क्योंकि टर्नस्टाइल के बायीं ओर के किसी भी परिसर को हमेशा दूसरी तरफ ले जाया जा सकता है और दोहरीकरण किया जा सकता है।

अब हम अनुमान नियम देते हैं जिसमें बताया गया है कि अनुक्रमों का प्रमाण कैसे बनाया जाए।^[4]

अब हम अनुक्रम कैलकुलस#अनुमान नियम देते हैं जिसमें बताया गया है कि अनुक्रमों का प्रमाण कैसे बनाया जाए।

सबसे पहले, इस तथ्य को औपचारिक रूप देने के लिए कि हम किसी संदर्भ में प्रस्तावों के क्रम की अवधान नहीं करते हैं, हम विनिमय का संरचनात्मक नियम जोड़ते हैं:

\vdash

\vdash

ध्यान दें कि हम अशक्त पड़ने और सिकुड़ने के संरचनात्मक नियमों को नहीं जोड़ते हैं, क्योंकि हम क्रम में प्रस्तावों की अनुपस्थिति और मौजूद प्रतियों की संख्या की अवधान करते हैं।

इसके बाद हम आरंभिक अनुक्रम और कट जोड़ते हैं:

\vdash

$\vdash$			$\vdash$

$\vdash$

कट नियम को प्रमाणों की रचना करने के एक तरीके के रूप में देखा जा सकता है, और प्रारंभिक अनुक्रम रचना के लिए इकाइयों के रूप में काम करते हैं। एक निश्चित अर्थ में, ये नियम निरर्थक हैं: जैसा कि हम नीचे साक्ष्य बनाने के लिए अतिरिक्त नियम पेश करते हैं, हम इस संपत्ति को बनाए रखेंगे कि स्वेच्छतः से प्रारंभिक अनुक्रम परमाणु प्रारंभिक अनुक्रमों से प्राप्त किए जा सकते हैं और जब भी कोई अनुक्रम सिद्ध हो तो उसे कट दिया जा सकता है- स्वतंत्र प्रमाण अंततः, यह विहित रूप गुण (जिसे परमाणु प्रारंभिक अनुक्रमों की पूर्णता और कट-उन्मूलन प्रमेय में विभाजित किया जा सकता है, जो विश्लेषणात्मक प्रमाण की धारणा को प्रेरित करता है) कंप्यूटर विज्ञान में रैखिक तर्क के अनुप्रयोगों के पीछे निहित है, क्योंकि यह तर्क की अनुमति देता है सबूत खोज में और संसाधन-जागरूक लैम्ब्डा-कैलकुलस के रूप में उपयोग किया जाता है।

अब हम तार्किक नियम देकर संयोजकों को समझाते हैं। आमतौर पर अनुक्रमिक कलन में, प्रत्येक संयोजक के लिए "दाएं-नियम" और "बाएं-नियम" दोनों दिए जाते हैं, अनिवार्य रूप से उस संयोजक से जुड़े प्रस्तावों के बारे में तर्क के दो तरीकों का वर्णन किया जाता है (जैसे, सत्यापन और मिथ्याकरण)। एकतरफ़ा प्रस्तुति में, इसके बजाय निषेध का उपयोग किया जाता है: संयोजक के लिए सही नियम (मान लीजिए ⅋) प्रभावी रूप से इसके दोहरे (⊗) के लिए बाएं नियमों की भूमिका निभाते हैं। इसलिए, हमें संयोजक के लिए नियम(नियमों) और उसके दोहरे नियम(नियमों) के बीच एक निश्चित "सामंजस्य" की अपेक्षा करनी चाहिए।

गुणक

गुणन समुच्चय (⊗) और वियोजन (⅋) के नियम:

$\vdash$			$\vdash$

$\vdash$

\vdash

\vdash

और उनकी इकाइयों के लिए:



$\vdash$

\vdash

\vdash

ध्यान दें कि गुणात्मक संयोजन और विच्छेदन के नियम चिरसम्मत व्याख्या के अंतर्गत सरल संयोजन और विच्छेदन के लिए स्वीकार्य हैं (यानी, वे एलके में स्वीकार्य नियम हैं)।

योजक

योगात्मक संयोजक (&) और वियोजन (⊕) के नियम:

$\vdash$			$\vdash$

$\vdash$

\vdash

\vdash

\vdash

\vdash

और उनकी इकाइयों के लिए:



$\vdash$

(0 के लिए कोई नियम नहीं)

ध्यान दें कि चिरसम्मत व्याख्या के तहत योगात्मक संयोजन और विच्छेदन के नियम फिर से स्वीकार्य हैं। लेकिन अब हम संयोजन के दो अलग-अलग संस्करणों के नियमों में गुणक/योगात्मक भेद के आधार को समझा सकते हैं: गुणक संयोजक (⊗) के लिए, निष्कर्ष का संदर्भ ( $Γ, Δ$ ) परिसर के बीच विभाजित है, जबकि एडिटिव केस कनेक्टिव (&) के लिए निष्कर्ष का संदर्भ ( $Γ$ ) दोनों परिसरों में संपूर्ण रूप से शामिल किया गया है।

घातांक

घातांक का उपयोग दुर्बलता और संकुचन तक नियंत्रित पहुँच देने के लिए किया जाता है। विशेष रूप से, हम ?'d प्रस्तावों के लिए अशक्त पड़ने और संकुचन के संरचनात्मक नियम जोड़ते हैं:^[5]

\vdash

\vdash

\vdash

\vdash

और निम्न तार्किक नियमों का उपयोग करें:

\vdash

\vdash

\vdash

\vdash

|}

कोई यह देख सकता है कि घातांक के नियम अन्य संयोजकों के नियमों से भिन्न पैटर्न का पालन करते हैं, सामान्य मोडल लॉजिक S4 के अनुक्रमिक कलन औपचारिकताओं में तौर-तरीकों को नियंत्रित करने वाले अनुमान नियमों से मिलते जुलते हैं, और अब इनके बीच इतनी स्पष्ट समरूपता नहीं है। दोहरे! और ?। इस स्थिति का समाधान सीएलएल की वैकल्पिक प्रस्तुतियों (जैसे, एलयू प्रस्तुति) में किया जाता है।

उल्लेखनीय सूत्र

ऊपर वर्णित डी मॉर्गन द्वंद्वों के अलावा, रैखिक तर्क में कुछ महत्वपूर्ण तुल्यताएं शामिल हैं:

वितरणशीलता

A \otimes (B \oplus C) ≣ (A \otimes B) \oplus (A \otimes C)

(A \oplus B) \otimes C ≣ (A \otimes C) \oplus (B \otimes C)

A ⅋ (B & C) ≣ (A ⅋ B) & (A ⅋ C)

(A & B) ⅋ C ≣ (A ⅋ C) & (B ⅋ C)

$A ⊸ B$ की $A ⊥ ⅋ B$ के रूप में परिभाषा के अनुसार, अंतिम दो वितरण नियम भी देते हैं:

A ⊸ (B & C) ≣ (A ⊸ B) & (A ⊸ C)

(A \oplus B) ⊸ C ≣ (A ⊸ C) & (B ⊸ C)

(यहाँ $A ≣ B$ है $(A ⊸ B) & (B ⊸ A)$ .)

घातीय समरूपता

!(A & B) ≣ ! A \otimes ! B

?(A \oplus B) ≣ ? A ⅋ ? B

रैखिक वितरण

एक प्रतिचित्र जो समरूपता नहीं है फिर भी रैखिक तर्क में एक महत्वपूर्ण भूमिका निभाता है:

(A \otimes (B ⅋ C)) ⊸ ((A \otimes B) ⅋ C)

रेखीय वितरण रेखीय तर्क के प्रमाण सिद्धांत में मौलिक हैं। इस मानचित्र के परिणामों की सबसे पहले जांच ^[6] में की गई और इसे "कमज़ोर वितरण" कहा गया। बाद के कार्य में रैखिक तर्क के साथ मूलभूत संबंध को दर्शाने के लिए इसका नाम बदलकर "रैखिक वितरण" कर दिया गया है।


अन्य निहितार्थ

निम्नलिखित वितरण सूत्र सामान्य रूप से एक तुल्यता नहीं हैं, केवल एक निहितार्थ हैं:

! A \otimes ! B ⊸ !(A \otimes B)

! A \oplus ! B ⊸ !(A \oplus B)

?(A ⅋ B) ⊸ ? A ⅋ ? B

?(A & B) ⊸ ? A & ? B

(A & B) \otimes C ⊸ (A \otimes C) & (B \otimes C)

(A & B) \oplus C ⊸ (A \oplus C) & (B \oplus C)

(A ⅋ C) \oplus (B ⅋ C) ⊸ (A \oplus B) ⅋ C

(A & C) \oplus (B & C) ⊸ (A \oplus B) & C

रैखिक तर्क में चिरसम्मत/अंतर्ज्ञानवादी तर्क को एन्कोड करना

अंतर्ज्ञानवादी और चिरसम्मत निहितार्थ दोनों को घातांक सम्मिलित करके रैखिक निहितार्थ से पुनर्प्राप्त किया जा सकता है: अंतर्ज्ञानवादी निहितार्थ को इस प्रकार एन्कोड किया गया है $! A ⊸ B$ , जबकि चिरसम्मत निहितार्थ को इस प्रकार एन्कोड किया जा सकता है $!? A ⊸ ? B$ या $! A ⊸ ?! B$ (या विभिन्न प्रकार के वैकल्पिक संभावित अनुवाद)।^[7] विचार यह है कि घातांक हमें एक सूत्र का जितनी बार आवश्यकता हो उतनी बार उपयोग करने की अनुमति देता है, जो चिरसम्मत और अंतर्ज्ञानवादी तर्क में हमेशा संभव है।

औपचारिक रूप से, अंतर्ज्ञानवादी तर्क के सूत्रों का रैखिक तर्क के सूत्रों में अनुवाद इस तरह से मौजूद है जो गारंटी देता है कि मूल सूत्र अंतर्ज्ञानवादी तर्क में सिद्ध करने योग्य है यदि और केवल तभी जब अनुवादित सूत्र रैखिक तर्क में सिद्ध हो। गोडेल-जेंटज़ेन ऋणात्मक अनुवाद का उपयोग करके, हम इस प्रकार चिरसम्मत प्रथम-क्रम तर्क को रैखिक प्रथम-क्रम तर्क में एम्बेड कर सकते हैं।

संसाधन व्याख्या

लाफोंट (1993) ने पहली बार दिखाया कि अंतर्ज्ञानवादी रैखिक तर्क को संसाधनों के तर्क के रूप में कैसे समझाया जा सकता है, इसलिए तार्किक भाषा को औपचारिकताओं तक पहुंच प्रदान करना जिसका उपयोग चिरसम्मत तर्क के बजाय, तर्क के भीतर संसाधनों के बारे में तर्क के लिए किया जा सकता है। गैर-तार्किक विधेय और संबंधों के साधन। इस विचार को स्पष्ट करने के लिए टोनी होरे (1985) के वेंडिंग मशीन के उत्कृष्ट उदाहरण का उपयोग किया जा सकता है।

मान लीजिए कि हम परमाणु प्रस्ताव द्वारा एक कैंडी बार का प्रतिनिधित्व करते हैं $candy$ , और एक डॉलर होने से $$1$ . इस तथ्य को बताने के लिए कि एक डॉलर आपको एक कैंडी बार खरीदेगा, हम निहितार्थ लिख सकते हैं $$1 \Rightarrow candy$ . लेकिन सामान्य (चिरसम्मत या अंतर्ज्ञानवादी) तर्क में, से $A$ और $A \Rightarrow B$ कोई निष्कर्ष निकाल सकता है $A \land B$ . तो, सामान्य तर्क हमें यह विश्वास दिलाता है कि हम कैंडी बार खरीद सकते हैं और अपना डॉलर रख सकते हैं! बिल्कुल, हम अधिक परिष्कृत एन्कोडिंग का उपयोग करके इस समस्या से बच सकते हैं,^{[clarification needed]} हालांकि आम तौर पर ऐसे एन्कोडिंग फ़्रेम समस्या से ग्रस्त होते हैं। हालाँकि, कमजोर पड़ने और संकुचन की अस्वीकृति रैखिक तर्क को भोले-भाले नियम के साथ भी इस तरह के नकली तर्क से बचने की अनुमति देती है। इसके बजाय $$1 \Rightarrow candy$ , हम वेंडिंग मशीन की संपत्ति को एक रैखिक निहितार्थ के रूप में व्यक्त करते हैं $$1 ⊸ candy$ . से $$1$ और इस तथ्य से हम निष्कर्ष निकाल सकते हैं $candy$ , लेकिन नहीं $$1 \otimes candy$ . सामान्य तौर पर, हम रैखिक तर्क प्रस्ताव का उपयोग कर सकते हैं $A ⊸ B$ परिवर्तित संसाधन की वैधता व्यक्त करने के लिए $A$ संसाधन में $B$ .

वेंडिंग मशीन के उदाहरण के साथ चलते हुए, अन्य गुणक और योगात्मक संयोजकों की संसाधन व्याख्याओं पर विचार करें। (घातांक इस संसाधन व्याख्या को निरंतर तार्किक सत्य की सामान्य धारणा के साथ संयोजित करने का साधन प्रदान करते हैं।)

गुणक समुच्चयबोधक $(A \otimes B)$ उपभोक्ता के निर्देशानुसार उपयोग किए जाने वाले संसाधनों की एक साथ घटना को दर्शाता है। उदाहरण के लिए, यदि आप गोंद की एक छड़ी और शीतल पेय की एक बोतल खरीदते हैं, तो आप अनुरोध कर रहे हैं $gum \otimes drink$ . स्थिरांक 1 किसी भी संसाधन की अनुपस्थिति को दर्शाता है, और इसलिए ⊗ की इकाई के रूप में कार्य करता है।

योगात्मक संयोजन $(A & B)$ संसाधनों की वैकल्पिक घटना का प्रतिनिधित्व करता है, जिसका चुनाव उपभोक्ता नियंत्रित करता है। यदि वेंडिंग मशीन में चिप्स का एक पैकेट, एक कैंडी बार और शीतल पेय की एक कैन है, प्रत्येक की कीमत एक डॉलर है, तो उस कीमत पर आप इनमें से बिल्कुल एक उत्पाद खरीद सकते हैं। इस प्रकार हम लिखते हैं $$1 ⊸ (candy & chips & drink)$ . हम नहीं लिखते $$1 ⊸ (candy \otimes chips \otimes drink)$ , जिसका अर्थ यह होगा कि तीनों उत्पादों को एक साथ खरीदने के लिए एक डॉलर पर्याप्त है। हालाँकि, से $$1 ⊸ (candy & chips & drink)$ , हम सही निष्कर्ष निकाल सकते हैं $$3 ⊸ (candy \otimes chips \otimes drink)$ , कहाँ $$3 := $1 \otimes $1 \otimes $1$ . योगात्मक संयोजन की इकाई ⊤ को कूड़े की टोकरी के रूप में देखा जा सकता है अनावश्यक संसाधनों के लिए. उदाहरण के लिए, हम लिख सकते हैं $$3 ⊸ (candy \otimes ⊤)$ यह व्यक्त करने के लिए कि तीन डॉलर से आप एक कैंडी बार और कुछ अन्य सामान प्राप्त कर सकते हैं, बिना अधिक विशिष्ट हुए (उदाहरण के लिए, चिप्स और एक पेय, या $2, या $1 और चिप्स, आदि)।

योगात्मक विभक्ति $(A \oplus B)$ संसाधनों की वैकल्पिक घटना का प्रतिनिधित्व करता है, जिसका चुनाव मशीन नियंत्रित करती है। उदाहरण के लिए, मान लीजिए कि वेंडिंग मशीन जुए की अनुमति देती है: एक डॉलर डालें और मशीन एक कैंडी बार, चिप्स का एक पैकेट या एक शीतल पेय दे सकती है। इस स्थिति को हम इस प्रकार व्यक्त कर सकते हैं $$1 ⊸ (candy \oplus chips \oplus drink)$ . स्थिरांक 0 एक ऐसे उत्पाद का प्रतिनिधित्व करता है जिसे बनाया नहीं जा सकता है, और इस प्रकार ⊕ की इकाई के रूप में कार्य करता है (एक मशीन जो उत्पादन कर सकती है) $A$ या $0$ एक मशीन की तरह अच्छा है जो हमेशा उत्पादन करती है $A$ क्योंकि यह कभी भी 0 उत्पन्न करने में सफल नहीं होगा)। इसलिए उपरोक्त के विपरीत, हम निष्कर्ष नहीं निकाल सकते $$3 ⊸ (candy \otimes chips \otimes drink)$ इस से।

गुणात्मक विभक्ति $(A ⅋ B)$ संसाधन व्याख्या के संदर्भ में स्पष्ट करना अधिक कठिन है, हालांकि हम रैखिक निहितार्थ में वापस एन्कोड कर सकते हैं, या तो $A ⊥ ⊸ B$ या $B ⊥ ⊸ A$ .

अन्य प्रमाण प्रणालियाँ

प्रमाण जाल

जीन-यवेस गिरार्ड द्वारा प्रस्तुत, नौकरशाही से बचने के लिए प्रमाण जाल बनाए गए हैं, यानी वे सभी चीजें जो तार्किक दृष्टिकोण से दो व्युत्पत्तियों को अलग बनाती हैं, लेकिन नैतिक दृष्टिकोण से नहीं।

उदाहरण के लिए, ये दोनों प्रमाण नैतिक रूप से समान हैं:

\vdash

\vdash

\vdash

\vdash

\vdash

\vdash

प्रूफ़ नेट का लक्ष्य उनका ग्राफिकल प्रतिनिधित्व बनाकर उन्हें समान बनाना है।

शब्दार्थ

बीजगणितीय शब्दार्थ

निर्णायकता/प्रवेश की जटिलता

पूर्ण सीएलएल में प्रवेश संबंध अनिर्णीत समस्या है।^[8] के अंशों पर विचार करते समय सीएलएल, निर्णय समस्या की जटिलता अलग-अलग है:

गुणक रैखिक तर्क (एमएलएल): केवल गुणक संयोजक। एमएलएल प्रवेश एनपी-पूर्ण है, यहां तक कि विशुद्ध रूप से निहितार्थ खंड में सींग उपवाक्य तक सीमित है,^[9] या परमाणु-मुक्त सूत्रों के लिए।^[10]
गुणक-योगात्मक रैखिक तर्क (MALL): केवल गुणक और योगात्मक (अर्थात, घातांक-मुक्त)। MALL प्रवेश PSPACE-पूर्ण है।^[8]* गुणक-घातांक रैखिक तर्क (एमईएल): केवल गुणक और घातांक। पेट्री डिश के लिए पहुंच की समस्या को कम करके,^[11] एमईएल प्रवेश कम से कम एक्सस्पेस |एक्सपस्पेस-कठिन होना चाहिए, हालांकि निर्णायकता को स्वयं एक लंबे समय से चली आ रही खुली समस्या का दर्जा प्राप्त है। 2015 में, सैद्धांतिक कंप्यूटर विज्ञान (पत्रिका)जर्नल) पत्रिका में निर्णायकता का प्रमाण प्रकाशित किया गया था।^[12] लेकिन बाद में इसे गलत बताया गया।^[13]
एफाइन लीनियर लॉजिक (अर्थात कमजोर पड़ने वाला रैखिक तर्क, एक टुकड़े के बजाय एक विस्तार) को 1995 में निर्णय लेने योग्य दिखाया गया था।^[14]

वेरिएंट

संरचनात्मक नियमों के साथ और छेड़छाड़ करने से रैखिक तर्क के कई रूप उत्पन्न होते हैं:

एफ़िन तर्क, जो संकुचन को रोकता है लेकिन वैश्विक कमज़ोरी (एक निर्णायक विस्तार) की अनुमति देता है।
सख्त तर्क या प्रासंगिक तर्क, जो कमजोर होने से रोकता है लेकिन वैश्विक संकुचन की अनुमति देता है।
नॉनकम्यूटेटिव तर्क |नॉनकम्यूटेटिव लॉजिक या ऑर्डर्ड लॉजिक, जो कमजोर पड़ने और संकुचन को रोकने के अलावा, विनिमय के नियम को हटा देता है। क्रमबद्ध तर्क में, रैखिक निहितार्थ आगे बाएँ-निहितार्थ और दाएँ-निहितार्थ में विभाजित होता है।

रैखिक तर्क के विभिन्न अंतर्ज्ञानवादी रूपों पर विचार किया गया है। जब एकल-निष्कर्ष अनुक्रमिक कैलकुलस प्रस्तुति पर आधारित होता है, जैसे ILL (अंतर्ज्ञानवादी रैखिक तर्क) में, संयोजक ⅋, ⊥, और ? अनुपस्थित हैं, और रैखिक निहितार्थ को एक आदिम संयोजक के रूप में माना जाता है। FILL (पूर्ण अंतर्ज्ञानवादी रैखिक तर्क) में संयोजक ⅋, ⊥, और ? मौजूद हैं, रैखिक निहितार्थ एक आदिम संयोजक है और, जैसा कि अंतर्ज्ञानवादी तर्क में होता है, सभी संयोजक (रैखिक निषेध को छोड़कर) स्वतंत्र हैं। रैखिक तर्क के प्रथम और उच्च-क्रम विस्तार भी हैं, जिनका औपचारिक विकास कुछ हद तक मानक है (प्रथम-क्रम तर्क और उच्च-क्रम तर्क देखें)।

यह भी देखें

चू स्थान
कम्प्यूटेबिलिटी तर्क
खेल शब्दार्थ
इंटरेक्शन की ज्यामिति
अंतर्ज्ञानवादी तर्क
रैखिक तर्क प्रोग्रामिंग
रैखिक प्रकार की प्रणाली, एक उपसंरचनात्मक प्रकार की प्रणाली
एकता का तर्क (एलयू)
लुडिक्स
सबूत जाल
विशिष्टता प्रकार

संदर्भ

↑ Girard, Jean-Yves (1987). "रेखीय तर्क" (PDF). Theoretical Computer Science. 50 (1): 1–102. doi:10.1016/0304-3975(87)90045-4. hdl:10338.dmlcz/120513.
↑ Baez, John; Stay, Mike (2008). Bob Coecke (ed.). "Physics, Topology, Logic and Computation: A Rosetta Stone" (PDF). New Structures of Physics.
↑ de Paiva, V.; van Genabith, J.; Ritter, E. (1999). Dagstuhl Seminar 99341 on Linear Logic and Applications (PDF). pp. 1–21. doi:10.4230/DagSemRep.248.
↑ Girard (1987), p.22, Def.1.15
↑ Girard (1987), p.25-26, Def.1.21
↑ J. Robin Cockett and Robert Seely "Weakly distributive categories" Journal of Pure and Applied Algebra 114(2) 133-173, 1997
↑ Di Cosmo, Roberto. The Linear Logic Primer. Course notes; chapter 2.
↑ ^8.0 ^8.1 For this result and discussion of some of the fragments below, see: Lincoln, Patrick; Mitchell, John; Scedrov, Andre; Shankar, Natarajan (1992). "Decision Problems for Propositional Linear Logic". Annals of Pure and Applied Logic. 56 (1–3): 239–311. doi:10.1016/0168-0072(92)90075-B.
↑ Kanovich, Max I. (1992-06-22). "रैखिक तर्क में हॉर्न प्रोग्रामिंग एनपी-पूर्ण है". Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings. Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings. pp. 200–210. doi:10.1109/LICS.1992.185533. ISBN 0-8186-2735-2.
↑ Lincoln, Patrick; Winkler, Timothy (1994). "लगातार-केवल गुणात्मक रैखिक तर्क एनपी-पूर्ण है". Theoretical Computer Science. 135: 155–169. doi:10.1016/0304-3975(94)00108-1.
↑ Gunter, C. A.; Gehlot, V. (1989). Tenth International Conference on Application and Theory of Petri Nets. Proceedings. pp. 174–191. {{cite conference}}: Missing or empty |title= (help)
↑ Bimbó, Katalin (2015-09-13). "शास्त्रीय रैखिक तर्क के गहन खंड की निर्णायकता". Theoretical Computer Science. 597: 1–17. doi:10.1016/j.tcs.2015.06.019. ISSN 0304-3975.
↑ Straßburger, Lutz (2019-05-10). "एमईएल के लिए निर्णय समस्या पर". Theoretical Computer Science. 768: 91–98. doi:10.1016/j.tcs.2019.02.022. ISSN 0304-3975.
↑ Kopylov, A. P. (1995-06-01). "रैखिक एफ़िन तर्क की निर्णायकता". Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings. Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings. pp. 496–504. CiteSeerX 10.1.1.23.9226. doi:10.1109/LICS.1995.523283. ISBN 0-8186-7050-9.

अग्रिम पठन

Girard, Jean-Yves. Linear logic, Theoretical Computer Science, Vol 50, no 1, pp. 1–102, 1987.
Girard, Jean-Yves, Lafont, Yves, and Taylor, Paul. Proofs and Types. Cambridge Press, 1989.
Hoare, C. A. R., 1985. Communicating Sequential Processes. Prentice-Hall International. ISBN 0-13-153271-5
Lafont, Yves, 1993. Introduction to Linear Logic. Lecture notes from TEMPUS Summer School on Algebraic and Categorical Methods in Computer Science, Brno, Czech Republic.
Troelstra, A.S. Lectures on Linear Logic. CSLI (Center for the Study of Language and Information) Lecture Notes No. 29. Stanford, 1992.
A. S. Troelstra, H. Schwichtenberg (1996). Basic Proof Theory. In series Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, ISBN 0-521-77911-1.
Di Cosmo, Roberto, and Danos, Vincent. The linear logic primer.
Introduction to Linear Logic (Postscript) by Patrick Lincoln
Introduction to Linear Logic by Torben Brauner
A taste of linear logic by Philip Wadler
Linear Logic by Roberto Di Cosmo and Dale Miller. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).
Overview of linear logic programming by Dale Miller. In Linear Logic in Computer Science, edited by Ehrhard, Girard, Ruet, and Scott. Cambridge University Press. London Mathematical Society Lecture Notes, Volume 316, 2004.
Linear Logic Wiki

बाहरी संबंध

Media related to रेखीय तर्क at Wikimedia Commons
A Linear Logic Prover (llprover) Archived 2016-04-04 at the Wayback Machine, available for use online, from: Naoyuki Tamura / Dept of CS / Kobe University / Japan

[1] Girard, Jean-Yves (1987). "रेखीय तर्क" (PDF). Theoretical Computer Science. 50 (1): 1–102. doi:10.1016/0304-3975(87)90045-4. hdl:10338.dmlcz/120513.

[2] Baez, John; Stay, Mike (2008). Bob Coecke (ed.). "Physics, Topology, Logic and Computation: A Rosetta Stone" (PDF). New Structures of Physics.

[3] Paiva, V.; van Genabith, J.; Ritter, E. (1999). Dagstuhl Seminar 99341 on Linear Logic and Applications (PDF). pp. 1–21. doi:10.4230/DagSemRep.248.

[4] Girard (1987), p.22, Def.1.15

[5] Girard (1987), p.25-26, Def.1.21

[6] J. Robin Cockett and Robert Seely "Weakly distributive categories" Journal of Pure and Applied Algebra 114(2) 133-173, 1997

[7] Di Cosmo, Roberto. The Linear Logic Primer. Course notes; chapter 2.

[Lincoln+92-8] 8.0 ^8.1 For this result and discussion of some of the fragments below, see: Lincoln, Patrick; Mitchell, John; Scedrov, Andre; Shankar, Natarajan (1992). "Decision Problems for Propositional Linear Logic". Annals of Pure and Applied Logic. 56 (1–3): 239–311. doi:10.1016/0168-0072(92)90075-B.

[9] Kanovich, Max I. (1992-06-22). "रैखिक तर्क में हॉर्न प्रोग्रामिंग एनपी-पूर्ण है". Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings. Seventh Annual IEEE Symposium on Logic in Computer Science, 1992. LICS '92. Proceedings. pp. 200–210. doi:10.1109/LICS.1992.185533. ISBN 0-8186-2735-2.

[10] Lincoln, Patrick; Winkler, Timothy (1994). "लगातार-केवल गुणात्मक रैखिक तर्क एनपी-पूर्ण है". Theoretical Computer Science. 135: 155–169. doi:10.1016/0304-3975(94)00108-1.

[11] Gunter, C. A.; Gehlot, V. (1989). Tenth International Conference on Application and Theory of Petri Nets. Proceedings. pp. 174–191. {{cite conference}}: Missing or empty |title= (help)

[12] Bimbó, Katalin (2015-09-13). "शास्त्रीय रैखिक तर्क के गहन खंड की निर्णायकता". Theoretical Computer Science. 597: 1–17. doi:10.1016/j.tcs.2015.06.019. ISSN 0304-3975.

[13] Straßburger, Lutz (2019-05-10). "एमईएल के लिए निर्णय समस्या पर". Theoretical Computer Science. 768: 91–98. doi:10.1016/j.tcs.2019.02.022. ISSN 0304-3975.

[14] Kopylov, A. P. (1995-06-01). "रैखिक एफ़िन तर्क की निर्णायकता". Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings. Tenth Annual IEEE Symposium on Logic in Computer Science, 1995. LICS '95. Proceedings. pp. 496–504. CiteSeerX 10.1.1.23.9226. doi:10.1109/LICS.1995.523283. ISBN 0-8186-7050-9.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

v t e Non-classical logic
Intuitionistic	Intuitionistic logic Constructive analysis Heyting arithmetic Intuitionistic type theory Constructive set theory
Fuzzy	Degree of truth Fuzzy rule Fuzzy set Fuzzy finite element Fuzzy set operations
Substructural	Structural rule Relevance logic Linear logic
Paraconsistent	Dialetheism
Description	Ontology (computer science) Ontology language
Many-valued	Three-valued Four-valued Łukasiewicz
Digital logic	Three-state logic Tri-state buffer Four-valued Verilog IEEE 1164 VHDL
Others	Dynamic semantics Inquisitive logic Intermediate logic Nonmonotonic logic

Anonymous

Search

रेखीय तर्क

Namespaces

More

Page actions

Contents

संयोजकता, द्वंद्व, और ध्रुवता

सिंटेक्स

अनुक्रमिक कलन प्रस्तुति

गुणक

योजक

घातांक

उल्लेखनीय सूत्र

रैखिक तर्क में चिरसम्मत/अंतर्ज्ञानवादी तर्क को एन्कोड करना

संसाधन व्याख्या

अन्य प्रमाण प्रणालियाँ

प्रमाण जाल

शब्दार्थ

बीजगणितीय शब्दार्थ

निर्णायकता/प्रवेश की जटिलता

वेरिएंट

यह भी देखें

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

रेखीय तर्क

संयोजकता, द्वंद्व, और ध्रुवता

सिंटेक्स

अनुक्रमिक कलन प्रस्तुति

गुणक

योजक

घातांक

उल्लेखनीय सूत्र

रैखिक तर्क में चिरसम्मत/अंतर्ज्ञानवादी तर्क को एन्कोड करना

संसाधन व्याख्या

अन्य प्रमाण प्रणालियाँ

प्रमाण जाल

शब्दार्थ

बीजगणितीय शब्दार्थ

निर्णायकता/प्रवेश की जटिलता

वेरिएंट

यह भी देखें

संदर्भ

अग्रिम पठन

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories