रेखीय तर्क

"⅋" 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⊥)

संयोजकों का वर्गीकरण

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

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

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

संयोजकों के व्याकरण में रैखिक निहितार्थ सम्मिलित नहीं है, लेकिन 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

$\vdash$ Γ

$\vdash$ Γ, ⊥

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

योजक

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

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

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

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

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

$\vdash$ Γ, ⊤

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

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

घातांक

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

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

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

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

$\vdash$ ?Γ, A

$\vdash$ ?Γ, !A

$\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: प्रमाण जालक

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

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

$\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: क्वान्टेल

निर्णय की जटिलता/जटिलता

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

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

वेरिएंट

संरचनात्मक नियमों के साथ और अधिक अपवृद्धि करने से रैखिक तर्क के कई रूप सामने आते हैं:

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

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

यह भी देखें

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

अग्रिम पठन

• 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