तार्किक रूपरेखा

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

सिंहावलोकन

एक तार्किक रूपरेखा आश्रित प्रकार के सिद्धांत के माध्यम से वाक्य रचना, नियमों और प्रमाणों के सामान्य उपचार पर आधारित है। सिंटेक्स को एक समान शैली में व्यवहार किया जाता है, किंतु प्रति मार्टिन-लोफ की प्रणाली की तुलना में अधिक सामान्य है।

एक तार्किक रूपरेखा का वर्णन करने के लिए, निम्नलिखित प्रदान करना होगा:

1. प्रतिनिधित्व किए जाने वाले ऑब्जेक्ट-लॉजिक्स के वर्ग का लक्षण वर्णन;
2. एक उपयुक्त मेटा-भाषा;
3. तंत्र का लक्षण वर्णन जिसके द्वारा ऑब्जेक्ट-लॉजिक्स का प्रतिनिधित्व किया जाता है।

इसका सारांश इस प्रकार है:

फ्रेमवर्क = भाषा + प्रतिनिधित्व।

एलएफ

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

एलऍफ़ लॉजिकल फ्रेमवर्क में लॉजिक को जजमेंट-एज-टाइप रिप्रेजेंटेशन मैकेनिज्म द्वारा दर्शाया जाता है। यह 1983 के सिएना लेक्चर्स में प्रति मार्टिन-लोफ के इम्मैनुएल कांत के फैसले की धारणा (गणितीय तर्क) के विकास से प्रेरित है। दो उच्च-क्रम के निर्णय, काल्पनिक $J\vdash K$ और जनरल, $\Lambda x\in J.K(x)$, क्रमशः साधारण और आश्रित कार्य स्थान के अनुरूप है। प्रकार के निर्णयों की पद्धति यह है कि निर्णयों को उनके प्रमाणों के प्रकारों के रूप में दर्शाया जाता है। तार्किक प्रणाली ${\mathcal {L}}$ इसके सिग्नेचर द्वारा दर्शाया जाता है जो स्थिरांकों के परिमित समुच्चय को प्रकार और प्रकार प्रदान करता है जो इसके सिंटैक्स, इसके निर्णय और इसकी नियम योजनाओं का प्रतिनिधित्व करता है। वस्तु-तर्क के नियमों और प्रमाणों को काल्पनिक-सामान्य निर्णयों के primitive प्रमाण $\Lambda x\in C.J(x)\vdash K$ के रूप में देखा जाता है।

कार्नेगी मेलन विश्वविद्यालय ट्वेलफ में ट्वेलफ प्रणाली द्वारा एलऍफ़ तार्किक रूपरेखा का कार्यान्वयन प्रदान किया गया है।

• एक तर्क प्रोग्रामिंग इंजन
• तर्क कार्यक्रमों (समाप्ति, कवरेज, आदि) के बारे में मेटा-सैद्धांतिक तर्क
• एक आगमनात्मक मेटा तर्क प्रमेय प्रोवर

यह भी देखें

• व्याकरणिक रूपरेखा
• टर्नस्टाइल (प्रतीक)

अग्रिम पठन

• Frank Pfenning (2002). "Logical frameworks – a brief introduction". In Helmut Schwichtenberg, Ralf Steinbrüggen (ed.). Proof and system-reliability (PDF). Springer. ISBN 978-1-4020-0608-1.
• Robert Harper, Furio Honsell and Gordon Plotkin. A Framework For Defining Logics. Journal of the Association for Computing Machinery, 40(1):143-184, 1993.
• Arnon Avron, Furio Honsell, Ian Mason and Randy Pollack. Using typed lambda calculus to implement formal systems on a machine. Journal of Automated Reasoning, 9:309-354, 1992.
• Robert Harper. An Equational Formulation of LF. Technical Report, University of Edinburgh, 1988. LFCS report ECS-LFCS-88-67.
• Robert Harper, Donald Sannella and Andrzej Tarlecki. Structured Theory Presentations and Logic Representations. Annals of Pure and Applied Logic, 67(1-3):113-160, 1994.
• Samin Ishtiaq and David Pym. A Relevant Analysis of Natural Deduction. Journal of Logic and Computation 8, 809-838, 1998.
• Samin Ishtiaq and David Pym. Kripke Resource Models of a Dependently-typed, Bunched $\lambda$-calculus. Journal of Logic and Computation 12(6), 1061-1104, 2002.
• Per Martin-Löf. "On the Meanings of the Logical Constants and the Justifications of the Logical Laws." "Nordic Journal of Philosophical Logic", 1(1): 11-60, 1996.
• Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. Oxford University Press, 1990. (The book is out of print, but a free version has been made available.)
• David Pym. A Note on the Proof Theory of the $\lambda \Pi$-calculus. Studia Logica 54: 199-230, 1995.
• David Pym and Lincoln Wallen. Proof-search in the $\lambda \Pi$-calculus. In: G. Huet and G. Plotkin (eds), Logical Frameworks, Cambridge University Press, 1991.
• Didier Galmiche and David Pym. Proof-search in type-theoretic languages:an introduction. Theoretical Computer Science 232 (2000) 5-53.
• Philippa Gardner. Representing Logics in Type Theory. Technical Report, University of Edinburgh, 1992. LFCS report ECS-LFCS-92-227.
• Gilles Dowek. The undecidability of typability in the lambda-pi-calculus. In M. Bezem, J.F. Groote (Eds.), Typed Lambda Calculi and Applications. Volume 664 of Lecture Notes in Computer Science, 139-145, 1993.
• David Pym. Proofs, Search and Computation in General Logic. Ph.D. thesis, University of Edinburgh, 1990.
• David Pym. A Unification Algorithm for the $\lambda \Pi$-calculus. International Journal of Foundations of Computer Science 3(3), 333-378, 1992.

बाहरी संबंध

• Specific Logical Frameworks and Implementations (a list maintained by Frank Pfenning, but mostly dead links from 1997)