औपचारिक प्रमाण

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

औपचारिक प्रमाण अक्सर इंटरैक्टिव प्रमेय साबित करना में कंप्यूटर की मदद से बनाए जाते हैं (उदाहरण के लिए, प्रूफ चेकर और स्वचालित प्रमेय प्रोवर के उपयोग के माध्यम से)। गौरतलब है कि इन प्रूफों को अपने आप ही, कंप्यूटर द्वारा भी चेक किया जा सकता है। औपचारिक प्रमाणों की जांच करना आमतौर पर सरल होता है, जबकि प्रमाणों को खोजने की समस्या (स्वचालित प्रमेय साबित करना) आमतौर पर उपयोग में औपचारिक प्रणाली के आधार पर कम्प्यूटेशनल रूप से अट्रैक्टिव # इंट्रेक्टेबिलिटी और/या केवल अर्ध-निर्णायक होती है।

पृष्ठभूमि

औपचारिक भाषा

Main article: Formal language

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

औपचारिक व्याकरण

Main articles: Formal grammar and Formation rule

एक औपचारिक व्याकरण (जिसे गठन नियम भी कहा जाता है) औपचारिक भाषा के अच्छी तरह से गठित सूत्रों का एक सटीक विवरण है। यह औपचारिक भाषा के वर्णमाला के ऊपर स्ट्रिंग (कंप्यूटर विज्ञान) के सेट का पर्याय है जो अच्छी तरह से गठित सूत्र बनाते हैं। हालाँकि, यह उनके शब्दार्थ (अर्थात उनका क्या मतलब है) का वर्णन नहीं करता है।

औपचारिक प्रणाली

Main article: Formal system

एक औपचारिक प्रणाली (जिसे लॉजिकल कैलकुलस या लॉजिकल सिस्टम भी कहा जाता है) में एक औपचारिक भाषा होती है, जिसमें एक डिडक्टिव उपकरण (जिसे एक डिडक्टिव सिस्टम भी कहा जाता है) होता है। कटौतीत्मक तंत्र में परिवर्तन नियमों का एक सेट (जिसे अनुमान नियम भी कहा जाता है) या सिद्धांतों का एक सेट शामिल हो सकता है, या दोनों हो सकते हैं। एक औपचारिक प्रणाली का उपयोग सिद्धांत को एक या एक से अधिक अन्य अभिव्यक्तियों से एक अभिव्यक्ति के लिए किया जाता है।

व्याख्या

Main articles: Formal semantics (logic) and Interpretation (logic)

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

यह भी देखें

• स्वयंसिद्ध प्रणाली
• औपचारिक सत्यापन
• गणितीय प्रमाण
• सबूत सहायक
• सबूत कैलकुलस
• सबूत सिद्धांत
• प्रमाण (सत्य)
• ब्राउन फैक्टर

इस पेज में लापता आंतरिक लिंक की सूची

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

बाहरी संबंध

• "A Special Issue on Formal Proof". Notices of the American Mathematical Society. December 2008.
• 2πix.com: Logic Part of a series of articles covering mathematics and logic.
• Archive of Formal Proofs
• Mizar Home Page