मिज़ार प्रणाली
| File:Mizar system logo.gif | |
Screenshot  Mizar MathWiki screenshot | |
| Paradigm | Declarative |
|---|---|
| द्वारा डिज़ाइन किया गया | Andrzej Trybulec |
| पहली प्रस्तुति | 1973 |
| टाइपिंग अनुशासन | Weak, static |
| फ़ाइल नाम एक्सटेंशनएस | .miz .voc |
| वेबसाइट | www.mizar.org |
| Influenced by | |
| Automath | |
| Influenced | |
| OMDoc, HOL Light and Coq mizar modes | |
मिज़ार प्रणाली में गणितीय परिभाषाएँ और प्रूफ़ लिखने के लिए औपचारिक भाषा, प्रूफ़ सहायक, जो इस भाषा में लिखे गए प्रमाणों की स्वचालित जाँच करने में सक्षम है, और गणितीय औपचारिकता की लाइब्रेरी सम्मिलित है, जिसका उपयोग नए प्रमेयों के प्रूफ़ में किया जा सकता है।[1] इस प्रणाली का रखरखाव और विकास मिज़ार प्रोजेक्ट द्वारा किया जाता है, जो पहले इसके संस्थापक आंद्रेज ट्रायबुलेक के निर्देशन में था।
2009 में मिज़ार गणितीय पुस्तकालय अस्तित्व में सख्ती से औपचारिक गणित का सबसे बड़ा सुसंगत निकाय था।[2]
इतिहास
मिज़ार प्रोजेक्ट का प्रारंभ 1973 के आसपास आंद्रेज ट्रायबुलेक द्वारा गणितीय स्थानीय भाषा के पुनर्निर्माण के प्रयास के रूप में की गई थी जिससे इसे कंप्यूटर द्वारा जांचा जा सके।[3] इसका वर्तमान लक्ष्य, मिज़ार प्रणाली के निरंतर विकास के अतिरिक्त, औपचारिक रूप से सत्यापित प्रमाणों की बड़ी लाइब्रेरी का सहयोगात्मक निर्माण है, जो आधुनिक गणित के अधिकांश मूल को कवर करता है। यह प्रभावशाली QED घोषणापत्र के अनुरूप है।[4]
वर्तमान में यह परियोजना बेलस्टॉक विश्वविद्यालय, पोलैंड, अलबर्टा विश्वविद्यालय, कनाडा और शिंशु विश्वविद्यालय, जापान के अनुसंधान समूहों द्वारा विकसित और रखरखाव की जाती है। जबकि मिज़ार प्रूफ चेकर ओनर बना रहता है।[5] मिज़ार गणितीय पुस्तकालय-औपचारिक गणित का विशाल निकाय जिसे उसने सत्यापित किया- लाइसेंस प्राप्त ओपन-सोर्स है।[6]
मिज़ार प्रणाली से संबंधित पेपर नियमित रूप से गणितीय औपचारिकीकरण अकादमिक समुदाय की सहकर्मी-समीक्षा पत्रिकाओं में दिखाई देते हैं। इनमें लॉजिक, व्याकरण और रेटोरिक, इंटेलिजेंट कंप्यूटर गणित, इंटरएक्टिव प्रमेय सिद्ध करना, स्वचालित तर्क पत्रिका और औपचारिक तर्क का जर्नल में अध्ययन सम्मिलित हैं।
मिज़ार भाषा
मिज़ार भाषा की विशिष्ट विशेषता इसकी पठनीयता है। जैसा कि गणितीय पाठ में आम है, यह शास्त्रीय तर्क और घोषणात्मक प्रोग्रामिंग पर निर्भर करता है।[7] मिज़ार लेख सामान्य ASCII में लिखे जाते हैं, लेकिन भाषा को गणितीय स्थानीय भाषा के इतना समीप डिज़ाइन किया गया था। कि अधिकांश गणितज्ञ विशेष प्रशिक्षण के बिना मिज़ार लेख पढ़ और समझ सकें।[1] फिर भी, भाषा स्वचालित प्रूफ़ जाँच के लिए आवश्यक औपचारिकता के बढ़े हुए स्तर को सक्षम बनाती है।
किसी प्रूफ़ को स्वीकार करने के लिए, सभी चरणों को या तो प्राथमिक तार्किक तर्कों द्वारा या पहले से सत्यापित प्रमाणों का हवाला देकर उचित ठहराया जाना चाहिए।[8] इसके परिणामस्वरूप गणितीय पाठ्यपुस्तकों और प्रकाशनों की तुलना में उच्च स्तर की कठोरता और विवरण प्राप्त होता है। इस प्रकार, विशिष्ट मिज़ार लेख सामान्य शैली में लिखे गए समकक्ष पेपर से लगभग चार गुना लंबा होता है।[9]
औपचारिकीकरण अपेक्षाकृत श्रमसाध्य है, लेकिन असंभव रूप से कठिन नहीं है। एक बार जब कोई व्यक्ति इस प्रणाली में पारंगत हो जाता है, तो पाठ्यपुस्तक पृष्ठ को औपचारिक रूप से सत्यापित करने में लगभग एक सप्ताह का पूर्णकालिक काम लगता है। इससे पता चलता है कि इसका लाभ अब संभाव्यता सिद्धांत और अर्थशास्त्र जैसे व्यावहारिक क्षेत्रों तक पहुंच में है।[2]
मिज़ार गणितीय पुस्तकालय
मिज़ार गणितीय लाइब्रेरी (एमएमएल) में सभी प्रमेय सम्मिलित हैं जिनका लेखक नए लिखे गए लेखों में उल्लेख कर सकते हैं। एक बार प्रूफ़ जांचकर्ता द्वारा अनुमोदित किए जाने के बाद उचित योगदान और शैली के लिए सहकर्मी-समीक्षा की प्रक्रिया में उनका आगे मूल्यांकन किया जाता है। यदि स्वीकार कर लिया जाता है तो उन्हें एसोसिएटेड जर्नल ऑफ फॉर्मलाइज्ड मैथमेटिक्स में प्रकाशित किया जाता है।[10] और एमएमएल में जोड़ा गया।
चौड़ाई
जुलाई 2012 तक, एमएमएल में 241 लेखकों द्वारा लिखे गए 1150 लेख सम्मिलित थे।[11] कुल मिलाकर, इनमें गणितीय वस्तुओं की 10,000 से अधिक औपचारिक परिभाषाएँ और इन वस्तुओं पर सिद्ध लगभग 52,000 प्रमेय सम्मिलित हैं। 180 से अधिक नामित गणितीय तथ्य औपचारिक संहिताकरण से लाभान्वित हुए हैं।[12] कुछ उदाहरण हैं हैन-बानाच प्रमेय, कोनिग की लेम्मा, ब्रौवर निश्चित बिंदु प्रमेय, गोडेल की पूर्णता प्रमेय और जॉर्डन वक्र प्रमेय है।
कवरेज की इस व्यापकता ने कुछ लोगों को आगे बढ़ाया है।[13] कंप्यूटर सत्यापन योग्य रूप में सभी मुख्य गणित को एन्कोड करने के QED घोषणापत्र के प्रमुख अनुमानों में से एक के रूप में मिज़ार का सुझाव देना।
उपलब्धता
सभी एमएमएल लेख औपचारिक गणित जर्नल के पेपर के रूप में पीडीएफ फॉर्म में उपलब्ध हैं।[10] एमएमएल का पूरा पाठ मिज़ार चेकर के साथ वितरित किया जाता है और इसे मिज़ार वेबसाइट से स्वतंत्र रूप से डाउनलोड किया जा सकता है। चल रहे हालिया प्रोजेक्ट में[14] पुस्तकालय को प्रायोगिक सप्ताह रूप में भी उपलब्ध कराया गया था।[15] यह केवल तभी संपादनों को स्वीकार करता है जब उन्हें मिज़ार चेकर द्वारा अनुमोदित किया जाता है।[16]
एमएमएल क्वेरी वेबसाइट[11] एमएमएल की सामग्री के लिए शक्तिशाली खोज इंजन प्रयुक्त करता है। अन्य क्षमताओं के अतिरिक्त, यह किसी विशेष प्रकार या ऑपरेटर के बारे में सिद्ध किए गए सभी एमएमएल प्रमेयों को पुनः प्राप्त कर सकता है।[17][18]
तार्किक संरचना
एमएमएल टार्स्की-ग्रोथेंडिक सेट सिद्धांत के सिद्धांतों पर बनाया गया है। सेट सिद्धांत में गणित के शब्दार्थ कार्यान्वयन के अतिरिक्त, भाषा किसी को कमजोर टाइपिंग को परिभाषित करने और उपयोग करने की अनुमति देती है। उदाहरण के लिए, किसी सेट को नेट प्रकार का तभी घोषित किया जा सकता है जब उसकी आंतरिक संरचना आवश्यकताओं की विशेष सूची के अनुरूप हो। बदले में, यह सूची प्राकृतिक संख्याओं की परिभाषा के रूप में कार्य करती है और इस सूची के अनुरूप सभी सेटों के सेट को NAT के रूप में दर्शाया जाता है।[19] प्रकारों का यह कार्यान्वयन अधिकांश गणितज्ञों द्वारा प्रतीकों के बारे में औपचारिक रूप से सोचने के विधियों को प्रतिबिंबित करना चाहता है।[20] और इसलिए संहिताकरण को सुव्यवस्थित करें।
मिज़ार प्रूफ चेकर
सभी प्रमुख ऑपरेटिंग प्रणाली के लिए मिज़ार प्रूफ़ चेकर के वितरण मिज़ार प्रोजेक्ट वेबसाइट पर डाउनलोड के लिए निःशुल्क उपलब्ध हैं। प्रूफ चेकर का उपयोग सभी गैर-व्यावसायिक उद्देश्यों के लिए निःशुल्क है। यह मुफ़्त पास्कल में लिखा गया है और स्रोत कोड मिज़ार उपयोगकर्ताओं के संघ के सभी सदस्यों के लिए उपलब्ध है।[21]
यह भी देखें
संदर्भ
- ↑ 1.0 1.1 Naumowicz, Adam; Artur Korniłowicz (2009). "मिज़ार का एक संक्षिप्त अवलोकन". Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science. 5674: 67–72. doi:10.1007/978-3-642-03359-9_5. ISBN 978-3-642-03358-2.
- ↑ 2.0 2.1 Wiedijk, Freek (2009). "एरो के प्रमेय को औपचारिक बनाना". Sādhanā. 34 (1): 193–220. doi:10.1007/s12046-009-0005-1. hdl:2066/75428.
- ↑ Matuszewski, Roman; Piotr Rudnicki (2005). "Mizar: the first 30 years" (PDF). Mechanized Mathematics and Its Applications. 4.
- ↑ Wiedijk, Freek. "बढ़ई". Retrieved 24 July 2018.
- ↑ Mailing list discussion Archived 2011-10-09 at the Wayback Machine referring to the close-sourcing of Mizar.
- ↑ Mailing list announcement referring to the open-sourcing of MML.
- ↑ Geuvers, H. (2009). "Proof assistants: History, ideas and future". Sādhanā. 34 (1): 3–25. doi:10.1007/s12046-009-0001-5.
- ↑ Wiedijk, Freek (2008). "औपचारिक प्रमाण--आरंभ करना" (PDF). Notices of the AMS. 55 (11): 1408–1414.
- ↑ Wiedijk, Freek. ""डी ब्रुइज़न फ़ैक्टर"". Retrieved 24 July 2018.
- ↑ 10.0 10.1 Journal of Formalized Mathematics
- ↑ 11.0 11.1 The MML Query search engine
- ↑ "एमएमएल में नामित प्रमेयों की एक सूची". Retrieved 22 July 2012.
- ↑ Wiedijk, Freek (2007). "QED घोषणापत्र पर दोबारा गौर किया गया". From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric. 10 (23).
- ↑ The MathWiki project homepage
- ↑ The MML in wiki form
- ↑ Alama, Jesse; Kasper Brink; Lionel Mamane; Josef Urban (2011). "Large Formal Wikis: Issues and Solutions". Intelligent Computer Mathematics. Lecture Notes in Computer Science. 6824: 133–148. arXiv:1107.3212. doi:10.1007/978-3-642-22673-1_10. ISBN 978-3-642-22672-4.
- ↑ An example of an MML query, yielding all theorems proved on the exponent operator, by the number of times they are cited in subsequent theorems.
- ↑ Another example of an MML query, yielding all theorems proved on sigma fields.
- ↑ Grabowski, Adam; Artur Kornilowicz; Adam Naumowicz (2010). "संक्षेप में बढ़ई". Journal of Formalized Reasoning. 3 (2): 152–245.
- ↑ Taylor, Paul (1999). गणित की व्यावहारिक नींव. Cambridge University Press. ISBN 9780521631075. Archived from the original on 2015-06-23. Retrieved 2012-07-24.
- ↑ The Association of Mizar Users website
