रेखीय तर्क

"⅋" redirects here. For ईपी, see ⅋ (ईपी).

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

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

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

सिंटेक्स

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

A	::=	p ∣ p⊥
	∣	A ⊗ A ∣ A ⊕ A
	∣	A & A ∣ A ⅋ A
	∣	1 ∣ 0 ∣ ⊤ ∣ ⊥
	∣	!A ∣ ?A

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

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

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

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

(p)⊥ = p⊥			(p⊥)⊥ = p
(A ⊗ B)⊥ = A⊥ ⅋ B⊥			(A ⅋ B)⊥ = A⊥ ⊗ B⊥
(A ⊕ B)⊥ = A⊥ & B⊥			(A & B)⊥ = A⊥ ⊕ B⊥
(1)⊥ = ⊥			(⊥)⊥ = 1
(0)⊥ = ⊤			(⊤)⊥ = 0
(!A)⊥ = ?(A⊥)			(?A)⊥ = !(A⊥)

Classification of connectives

	add	mul	exp
pos	⊕ 0	⊗ 1	!
neg	& ⊤	⅋ ⊥	?

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

तालिका के कॉलम रैखिक तर्क के संयोजकों को वर्गीकृत करने का एक और तरीका सुझाते हैं, जिसे ध्रुवीयता कहा जाता है: बाएं कॉलम में संयोजक नकारात्मक हैं

  (⊗, ⊕, 1, 0, !) को सकारात्मक कहा जाता है, जबकि दाहिनी ओर उनके दोहरे (⅋, &, ⊥, ⊤, ?) को नकारात्मक कहा जाता है; दाहिनी ओर सीएफ तालिका।

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

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

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

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

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

$\vdash$ Γ, A1, A2, Δ

$\vdash$ Γ, A2, A1, Δ

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

आगे हम प्रारंभिक अनुक्रम और कटौती जोड़ते हैं:

$\vdash$ A, A⊥

$\vdash$ Γ, A       $\vdash$ A⊥, Δ $\vdash$ Γ, Δ

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

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

गुणक

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

$\vdash$ Γ, A       $\vdash$ Δ, B $\vdash$ Γ, Δ, A ⊗ B

$\vdash$ Γ, A, B $\vdash$ Γ, A ⅋ B

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

| स्टाइल = मार्जिन: ऑटो |- | शैली = पाठ-संरेखण: केंद्र; |

$\vdash$ 1

| चौड़ाई = 50 | | शैली = पाठ-संरेखण: केंद्र; |

$\vdash$ Γ

$\vdash$ Γ, ⊥

|}

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

योजक

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

$\vdash$ Γ, A       $\vdash$ Γ, B $\vdash$ Γ, A & B

$\vdash$ Γ, A $\vdash$ Γ, A ⊕ B

$\vdash$ Γ, B $\vdash$ Γ, A ⊕ B

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

| स्टाइल = मार्जिन: ऑटो |- | शैली = पाठ-संरेखण: केंद्र; |

$\vdash$ Γ, ⊤

| चौड़ाई = 50 | | शैली = पाठ-संरेखण: केंद्र; | (इसके लिए कोई नियम नहीं) 0) |}

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

घातांक

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

$\vdash$ Γ $\vdash$ Γ, ?A

$\vdash$ Γ, ?A, ?A $\vdash$ Γ, ?A

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

| स्टाइल = मार्जिन: ऑटो |- | शैली = पाठ-संरेखण: केंद्र; |

$\vdash$ ?Γ, A

$\vdash$ ?Γ, !A

| चौड़ाई = 50 | | शैली = पाठ-संरेखण: केंद्र; |

$\vdash$ Γ, A

$\vdash$ Γ, ?A

|}

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

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

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

वितरणशीलता

A ⊗ (B ⊕ C) ≣ (A ⊗ B) ⊕ (A ⊗ C)

(A ⊕ B) ⊗ C ≣ (A ⊗ C) ⊕ (B ⊗ 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 ⊕ B) ⊸ C ≣ (A ⊸ C) & (B ⊸ C)

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

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

!(A & B) ≣ !A ⊗ !B

?(A ⊕ B) ≣ ?A ⅋ ?B

रैखिक वितरण

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

(A ⊗ (B ⅋ C)) ⊸ ((A ⊗ B) ⅋ C)

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

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

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

!A ⊗ !B ⊸ !(A ⊗ B)

!A ⊕ !B ⊸ !(A ⊕ B)

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

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

(A & B) ⊗ C ⊸ (A ⊗ C) & (B ⊗ C)

(A & B) ⊕ C ⊸ (A ⊕ C) & (B ⊕ C)

(A ⅋ C) ⊕ (B ⅋ C) ⊸ (A ⊕ B) ⅋ C

(A & C) ⊕ (B & C) ⊸ (A ⊕ B) & C

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

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

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

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

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

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

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

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

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

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

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

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

प्रमाण जाल

Main article: Proof net

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

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

$\vdash$ A, B, C, D $\vdash$ A ⅋ B, C, D $\vdash$ A ⅋ B, C ⅋ D

$\vdash$ A, B, C, D $\vdash$ A, B, C ⅋ D $\vdash$ A ⅋ B, C ⅋ D

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

शब्दार्थ

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

See also: Quantale

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

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

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

वेरिएंट

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

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

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

यह भी देखें

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

अग्रिम पठन

• 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