रैखिक तर्क

"⅋" redirects here. For the EP, see ⅋ (EP).

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

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

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

सिंटेक्स

शास्त्रीय रेखीय तर्क (सीएलएल) की भाषा को बैकस-नौर फॉर्म द्वारा अनिवार्य रूप से परिभाषित किया गया है

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

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

Symbol	Name
⊗	multiplicative conjunction	times	tensor
⊕	additive disjunction	plus
&	additive conjunction	with
⅋	multiplicative disjunction	par
!	of course	bang
?	why not

बाइनरी संयोजक ⊗, ⊕, & और ⅋ साहचर्य और क्रमविनिमेय हैं; 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.

तालिका के स्तंभ रैखिक तर्क के संयोजकों को वर्गीकृत करने का एक और तरीका सुझाते हैं, जिसे कहा जाता है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

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

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

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

वेरिएंट

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

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

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

यह भी देखें

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

अग्रिम पठन

• 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