मिज़ार प्रणाली: Difference between revisions

From Vigyanwiki
(Created page with "{{for|the star system|Mizar (star)}} {{Infobox programming language | name = Mizar | logo = File:Mizar system logo.gif | logo captio...")
 
No edit summary
Line 1: Line 1:
{{for|the star system|Mizar (star)}}
{{for|तारा प्रणाली|मिज़ार (स्टार)}}
{{Infobox programming language
{{Infobox programming language
  | name                  = Mizar
  | name                  = Mizar
Line 30: Line 30:
}}
}}


मिज़ार प्रणाली में गणितीय परिभाषाएँ और प्रमाण लिखने के लिए एक [[औपचारिक भाषा]], एक [[प्रमाण सहायक]], जो इस भाषा में लिखे गए प्रमाणों की स्वचालित जाँच करने में सक्षम है, और गणितीय औपचारिकता की एक लाइब्रेरी शामिल है, जिसका उपयोग नए प्रमेयों के प्रमाण में किया जा सकता है।<ref name="A Brief Overview of Mizar">{{cite journal | last = Naumowicz | first = Adam |author2=Artur Korniłowicz | title = मिज़ार का एक संक्षिप्त अवलोकन| journal = Theorem Proving in Higher Order Logics | year = 2009 | volume = 5674 | pages = 67–72 | series = Lecture Notes in Computer Science | doi=10.1007/978-3-642-03359-9_5| isbn = 978-3-642-03358-2 }}</ref> इस प्रणाली का रखरखाव और विकास मिज़ार प्रोजेक्ट द्वारा किया जाता है, जो पहले इसके संस्थापक [[आंद्रेज ट्रायबुलेक]] के निर्देशन में था।
मिज़ार प्रणाली में गणितीय परिभाषाएँ और प्रमाण लिखने के लिए एक [[औपचारिक भाषा]], एक [[प्रमाण सहायक]], जो इस भाषा में लिखे गए प्रमाणों की स्वचालित जाँच करने में सक्षम है, और गणितीय औपचारिकता की एक लाइब्रेरी सम्मिलित है, जिसका उपयोग नए प्रमेयों के प्रमाण में किया जा सकता है।<ref name="A Brief Overview of Mizar">{{cite journal | last = Naumowicz | first = Adam |author2=Artur Korniłowicz | title = मिज़ार का एक संक्षिप्त अवलोकन| journal = Theorem Proving in Higher Order Logics | year = 2009 | volume = 5674 | pages = 67–72 | series = Lecture Notes in Computer Science | doi=10.1007/978-3-642-03359-9_5| isbn = 978-3-642-03358-2 }}</ref> इस प्रणाली का रखरखाव और विकास मिज़ार प्रोजेक्ट द्वारा किया जाता है, जो पहले इसके संस्थापक [[आंद्रेज ट्रायबुलेक]] के निर्देशन में था।


2009 में मिज़ार गणितीय पुस्तकालय अस्तित्व में सख्ती से औपचारिक गणित का सबसे बड़ा सुसंगत निकाय था।<ref name="Arrow">{{cite journal | last = Wiedijk | first = Freek | title = एरो के प्रमेय को औपचारिक बनाना| journal = [[Sādhanā (journal)|Sādhanā]] | year = 2009 | volume = 34 | pages = 193–220 | issue = 1 | doi=10.1007/s12046-009-0005-1| hdl = 2066/75428 | doi-access = free }}</ref>
2009 में मिज़ार गणितीय पुस्तकालय अस्तित्व में सख्ती से औपचारिक गणित का सबसे बड़ा सुसंगत निकाय था।<ref name="Arrow">{{cite journal | last = Wiedijk | first = Freek | title = एरो के प्रमेय को औपचारिक बनाना| journal = [[Sādhanā (journal)|Sādhanā]] | year = 2009 | volume = 34 | pages = 193–220 | issue = 1 | doi=10.1007/s12046-009-0005-1| hdl = 2066/75428 | doi-access = free }}</ref>
Line 37: Line 37:
== इतिहास ==
== इतिहास ==


मिज़ार प्रोजेक्ट की शुरुआत 1973 के आसपास आंद्रेज ट्रायबुलेक द्वारा गणितीय स्थानीय भाषा के पुनर्निर्माण के प्रयास के रूप में की गई थी ताकि इसे कंप्यूटर द्वारा जांचा जा सके।<ref>{{cite journal | last = Matuszewski | first = Roman |author2=Piotr Rudnicki | title = Mizar: the first 30 years | journal = Mechanized Mathematics and Its Applications | year = 2005 | volume = 4 | url = http://mizar.org/people/romat/MatRud2005.pdf}}</ref> इसका वर्तमान लक्ष्य, मिज़ार प्रणाली के निरंतर विकास के अलावा, औपचारिक रूप से सत्यापित प्रमाणों की एक बड़ी लाइब्रेरी का सहयोगात्मक निर्माण है, जो आधुनिक गणित के अधिकांश मूल को कवर करता है। यह प्रभावशाली QED घोषणापत्र के अनुरूप है।<ref>{{cite web | last = Wiedijk | first = Freek | title = बढ़ई| url = https://www.cs.ru.nl/~freek/mizar/ | accessdate = 24 July 2018}}</ref>
मिज़ार प्रोजेक्ट का प्रारंभ 1973 के आसपास आंद्रेज ट्रायबुलेक द्वारा गणितीय स्थानीय भाषा के पुनर्निर्माण के प्रयास के रूप में की गई थी जिससे इसे कंप्यूटर द्वारा जांचा जा सके।<ref>{{cite journal | last = Matuszewski | first = Roman |author2=Piotr Rudnicki | title = Mizar: the first 30 years | journal = Mechanized Mathematics and Its Applications | year = 2005 | volume = 4 | url = http://mizar.org/people/romat/MatRud2005.pdf}}</ref> इसका वर्तमान लक्ष्य, मिज़ार प्रणाली के निरंतर विकास के अतिरिक्त, औपचारिक रूप से सत्यापित प्रमाणों की एक बड़ी लाइब्रेरी का सहयोगात्मक निर्माण है, जो आधुनिक गणित के अधिकांश मूल को कवर करता है। यह प्रभावशाली QED घोषणापत्र के अनुरूप है।<ref>{{cite web | last = Wiedijk | first = Freek | title = बढ़ई| url = https://www.cs.ru.nl/~freek/mizar/ | accessdate = 24 July 2018}}</ref>
 
वर्तमान में यह परियोजना बेलस्टॉक विश्वविद्यालय, पोलैंड, [[अलबर्टा विश्वविद्यालय]], कनाडा और [[शिंशु विश्वविद्यालय]], जापान के अनुसंधान समूहों द्वारा विकसित और रखरखाव की जाती है। जबकि मिज़ार प्रूफ चेकर मालिकाना बना रहता है,<ref name="not-open-source">[http://old.nabble.com/TPHOLs-becomes-ITP-%28fwd%29-td19435554.html#a19493250 Mailing list discussion] {{webarchive|url=https://web.archive.org/web/20111009115553/http://old.nabble.com/TPHOLs-becomes-ITP-(fwd)-td19435554.html |date=2011-10-09 }} referring to the close-sourcing of Mizar.</ref> मिज़ार गणितीय पुस्तकालय-औपचारिक गणित का विशाल निकाय जिसे उसने सत्यापित किया- लाइसेंस प्राप्त ओपन-सोर्स है।<ref name="library-open-source">[http://mizar.uwb.edu.pl/forum/archive/1104/msg00000.html Mailing list announcement] referring to the open-sourcing of MML.</ref>
वर्तमान में यह परियोजना बेलस्टॉक विश्वविद्यालय, पोलैंड, [[अलबर्टा विश्वविद्यालय]], कनाडा और [[शिंशु विश्वविद्यालय]], जापान के अनुसंधान समूहों द्वारा विकसित और रखरखाव की जाती है। जबकि मिज़ार प्रूफ चेकर मालिकाना बना रहता है,<ref name="not-open-source">[http://old.nabble.com/TPHOLs-becomes-ITP-%28fwd%29-td19435554.html#a19493250 Mailing list discussion] {{webarchive|url=https://web.archive.org/web/20111009115553/http://old.nabble.com/TPHOLs-becomes-ITP-(fwd)-td19435554.html |date=2011-10-09 }} referring to the close-sourcing of Mizar.</ref> मिज़ार गणितीय पुस्तकालय-औपचारिक गणित का विशाल निकाय जिसे उसने सत्यापित किया- लाइसेंस प्राप्त ओपन-सोर्स है।<ref name="library-open-source">[http://mizar.uwb.edu.pl/forum/archive/1104/msg00000.html Mailing list announcement] referring to the open-sourcing of MML.</ref>
मिज़ार प्रणाली से संबंधित पेपर नियमित रूप से गणितीय औपचारिकीकरण अकादमिक समुदाय की सहकर्मी-समीक्षा पत्रिकाओं में दिखाई देते हैं। इनमें लॉजिक, व्याकरण और रेटोरिक, इंटेलिजेंट कंप्यूटर गणित, [[इंटरएक्टिव प्रमेय सिद्ध करना]], [[स्वचालित तर्क पत्रिका]] और [[औपचारिक तर्क का जर्नल]] में अध्ययन शामिल हैं।
 
मिज़ार प्रणाली से संबंधित पेपर नियमित रूप से गणितीय औपचारिकीकरण अकादमिक समुदाय की सहकर्मी-समीक्षा पत्रिकाओं में दिखाई देते हैं। इनमें लॉजिक, व्याकरण और रेटोरिक, इंटेलिजेंट कंप्यूटर गणित, [[इंटरएक्टिव प्रमेय सिद्ध करना]], [[स्वचालित तर्क पत्रिका]] और [[औपचारिक तर्क का जर्नल]] में अध्ययन सम्मिलित हैं।


== मिज़ार भाषा ==
== मिज़ार भाषा ==


मिज़ार भाषा की विशिष्ट विशेषता इसकी पठनीयता है। जैसा कि गणितीय पाठ में आम है, यह [[शास्त्रीय तर्क]] और [[घोषणात्मक प्रोग्रामिंग]] पर निर्भर करता है।<ref>{{cite journal | last = Geuvers | first = H. | title = Proof assistants: History, ideas and future | journal = Sādhanā | year = 2009 | volume = 34 | issue = 1 | pages = 3–25 | doi = 10.1007/s12046-009-0001-5 | doi-access = free }}</ref> मिज़ार लेख सामान्य [[ASCII]] में लिखे जाते हैं, लेकिन भाषा को गणितीय स्थानीय भाषा के इतना करीब डिज़ाइन किया गया था कि अधिकांश गणितज्ञ विशेष प्रशिक्षण के बिना मिज़ार लेख पढ़ और समझ सकें।<ref name="A Brief Overview of Mizar"/>फिर भी, भाषा स्वचालित प्रूफ़ जाँच के लिए आवश्यक औपचारिकता के बढ़े हुए स्तर को सक्षम बनाती है।
मिज़ार भाषा की विशिष्ट विशेषता इसकी पठनीयता है। जैसा कि गणितीय पाठ में आम है, यह [[शास्त्रीय तर्क]] और [[घोषणात्मक प्रोग्रामिंग]] पर निर्भर करता है।<ref>{{cite journal | last = Geuvers | first = H. | title = Proof assistants: History, ideas and future | journal = Sādhanā | year = 2009 | volume = 34 | issue = 1 | pages = 3–25 | doi = 10.1007/s12046-009-0001-5 | doi-access = free }}</ref> मिज़ार लेख सामान्य [[ASCII]] में लिखे जाते हैं, लेकिन भाषा को गणितीय स्थानीय भाषा के इतना समीप डिज़ाइन किया गया था कि अधिकांश गणितज्ञ विशेष प्रशिक्षण के बिना मिज़ार लेख पढ़ और समझ सकें।<ref name="A Brief Overview of Mizar"/>फिर भी, भाषा स्वचालित प्रमाण जाँच के लिए आवश्यक औपचारिकता के बढ़े हुए स्तर को सक्षम बनाती है।


किसी प्रमाण को स्वीकार करने के लिए, सभी चरणों को या तो प्राथमिक तार्किक तर्कों द्वारा या पहले से सत्यापित प्रमाणों का हवाला देकर उचित ठहराया जाना चाहिए।<ref>{{cite journal | last = Wiedijk | first = Freek | title = औपचारिक प्रमाण--आरंभ करना| journal = Notices of the AMS |volume=55 |issue=11 |pages=1408–1414 | year = 2008 | url = https://www.ams.org/notices/200811/tx081101408p.pdf}}</ref> इसके परिणामस्वरूप गणितीय पाठ्यपुस्तकों और प्रकाशनों की तुलना में उच्च स्तर की कठोरता और विवरण प्राप्त होता है। इस प्रकार, एक विशिष्ट मिज़ार लेख सामान्य शैली में लिखे गए समकक्ष पेपर से लगभग चार गुना लंबा होता है।<ref>{{cite web | last = Wiedijk | first = Freek | title = "डी ब्रुइज़न फ़ैक्टर"| url = https://www.cs.ru.nl/~freek/factor/index.html | accessdate = 24 July 2018}}</ref>
किसी प्रमाण को स्वीकार करने के लिए, सभी चरणों को या तो प्राथमिक तार्किक तर्कों द्वारा या पहले से सत्यापित प्रमाणों का हवाला देकर उचित ठहराया जाना चाहिए।<ref>{{cite journal | last = Wiedijk | first = Freek | title = औपचारिक प्रमाण--आरंभ करना| journal = Notices of the AMS |volume=55 |issue=11 |pages=1408–1414 | year = 2008 | url = https://www.ams.org/notices/200811/tx081101408p.pdf}}</ref> इसके परिणामस्वरूप गणितीय पाठ्यपुस्तकों और प्रकाशनों की तुलना में उच्च स्तर की कठोरता और विवरण प्राप्त होता है। इस प्रकार, एक विशिष्ट मिज़ार लेख सामान्य शैली में लिखे गए समकक्ष पेपर से लगभग चार गुना लंबा होता है।<ref>{{cite web | last = Wiedijk | first = Freek | title = "डी ब्रुइज़न फ़ैक्टर"| url = https://www.cs.ru.nl/~freek/factor/index.html | accessdate = 24 July 2018}}</ref>
औपचारिकीकरण अपेक्षाकृत श्रमसाध्य है, लेकिन असंभव रूप से कठिन नहीं है। एक बार जब कोई व्यक्ति इस प्रणाली में पारंगत हो जाता है, तो पाठ्यपुस्तक पृष्ठ को औपचारिक रूप से सत्यापित करने में लगभग एक सप्ताह का पूर्णकालिक काम लगता है। इससे पता चलता है कि इसका लाभ अब संभाव्यता सिद्धांत और [[अर्थशास्त्र]] जैसे व्यावहारिक क्षेत्रों तक पहुंच में है।<ref name="Arrow"/>
 
औपचारिकीकरण अपेक्षाकृत श्रमसाध्य है, लेकिन असंभव रूप से कठिन नहीं है। एक बार जब कोई व्यक्ति इस प्रणाली में पारंगत हो जाता है, तो पाठ्यपुस्तक पृष्ठ को औपचारिक रूप से सत्यापित करने में लगभग एक सप्ताह का पूर्णकालिक काम लगता है। इससे पता चलता है कि इसका लाभ अब संभाव्यता सिद्धांत और [[अर्थशास्त्र]] जैसे व्यावहारिक क्षेत्रों तक पहुंच में है।<ref name="Arrow" />
 




== मिज़ार गणितीय पुस्तकालय ==
== मिज़ार गणितीय पुस्तकालय ==


मिज़ार गणितीय लाइब्रेरी (एमएमएल) में सभी प्रमेय शामिल हैं जिनका लेखक नए लिखे गए लेखों में उल्लेख कर सकते हैं। एक बार प्रूफ जांचकर्ता द्वारा अनुमोदित किए जाने के बाद उचित योगदान और शैली के लिए सहकर्मी-समीक्षा की प्रक्रिया में उनका आगे मूल्यांकन किया जाता है। यदि स्वीकार कर लिया जाता है तो उन्हें एसोसिएटेड जर्नल ऑफ फॉर्मलाइज्ड मैथमेटिक्स में प्रकाशित किया जाता है<ref name="Journal of Formalized Mathematics">[http://fm.mizar.org/ ''Journal of Formalized Mathematics'']</ref> और एमएमएल में जोड़ा गया।
मिज़ार गणितीय लाइब्रेरी (MML) में सभी प्रमेय सम्मिलित हैं जिनका लेखक नए लिखे गए लेखों में उल्लेख कर सकते हैं। एक बार प्रमाण जांचकर्ता द्वारा अनुमोदित किए जाने के बाद उचित योगदान और शैली के लिए सहकर्मी-समीक्षा की प्रक्रिया में उनका आगे मूल्यांकन किया जाता है। यदि स्वीकार कर लिया जाता है तो उन्हें एसोसिएटेड जर्नल ऑफ फॉर्मलाइज्ड मैथमेटिक्स में प्रकाशित किया जाता है<ref name="Journal of Formalized Mathematics">[http://fm.mizar.org/ ''Journal of Formalized Mathematics'']</ref> और एमएमएल में जोड़ा गया।


=== चौड़ाई ===
=== चौड़ाई ===


जुलाई 2012 तक, एमएमएल में 241 लेखकों द्वारा लिखे गए 1150 लेख शामिल थे।<ref name="MML Query">[http://mmlquery.mizar.org The MML Query search engine]</ref> कुल मिलाकर, इनमें गणितीय वस्तुओं की 10,000 से अधिक औपचारिक परिभाषाएँ और इन वस्तुओं पर सिद्ध लगभग 52,000 प्रमेय शामिल हैं। 180 से अधिक नामित गणितीय तथ्य औपचारिक संहिताकरण से लाभान्वित हुए हैं।<ref name="MML facts">{{cite web | title = एमएमएल में नामित प्रमेयों की एक सूची| url = http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename=mml-facts.mqt&argument=number+102 | accessdate = 22 July 2012}}</ref> कुछ उदाहरण हैं हैन-बानाच प्रमेय, कोनिग की लेम्मा, [[ब्रौवर निश्चित बिंदु प्रमेय]], गोडेल की पूर्णता प्रमेय और [[जॉर्डन वक्र प्रमेय]]।
जुलाई 2012 तक, एमएमएल में 241 लेखकों द्वारा लिखे गए 1150 लेख सम्मिलित थे।<ref name="MML Query">[http://mmlquery.mizar.org The MML Query search engine]</ref> कुल मिलाकर, इनमें गणितीय वस्तुओं की 10,000 से अधिक औपचारिक परिभाषाएँ और इन वस्तुओं पर सिद्ध लगभग 52,000 प्रमेय सम्मिलित हैं। 180 से अधिक नामित गणितीय तथ्य औपचारिक संहिताकरण से लाभान्वित हुए हैं।<ref name="MML facts">{{cite web | title = एमएमएल में नामित प्रमेयों की एक सूची| url = http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename=mml-facts.mqt&argument=number+102 | accessdate = 22 July 2012}}</ref> कुछ उदाहरण हैं हैन-बानाच प्रमेय, कोनिग की लेम्मा, [[ब्रौवर निश्चित बिंदु प्रमेय]], गोडेल की पूर्णता प्रमेय और [[जॉर्डन वक्र प्रमेय]] है।


कवरेज की इस व्यापकता ने कुछ लोगों को आगे बढ़ाया है<ref>{{cite journal | last = Wiedijk | first = Freek | title = QED घोषणापत्र पर दोबारा गौर किया गया| journal = From Insight to Proof: Festschrift in Honour of Andrzej Trybulec | year = 2007 | volume = 10 | series = [[Studies in Logic, Grammar and Rhetoric]] | issue = 23 | url = http://logika.uwb.edu.pl/studies/vol23.html}}</ref> कंप्यूटर सत्यापन योग्य रूप में सभी मुख्य गणित को एन्कोड करने के QED घोषणापत्र के प्रमुख अनुमानों में से एक के रूप में मिज़ार का सुझाव देना।
कवरेज की इस व्यापकता ने कुछ लोगों को आगे बढ़ाया है<ref>{{cite journal | last = Wiedijk | first = Freek | title = QED घोषणापत्र पर दोबारा गौर किया गया| journal = From Insight to Proof: Festschrift in Honour of Andrzej Trybulec | year = 2007 | volume = 10 | series = [[Studies in Logic, Grammar and Rhetoric]] | issue = 23 | url = http://logika.uwb.edu.pl/studies/vol23.html}}</ref> कंप्यूटर सत्यापन योग्य रूप में सभी मुख्य गणित को एन्कोड करने के QED घोषणापत्र के प्रमुख अनुमानों में से एक के रूप में मिज़ार का सुझाव देना।
Line 61: Line 65:
=== उपलब्धता ===
=== उपलब्धता ===


सभी एमएमएल लेख औपचारिक गणित जर्नल के पेपर के रूप में [[पीडीएफ]] फॉर्म में उपलब्ध हैं।<ref name="Journal of Formalized Mathematics"/>एमएमएल का पूरा पाठ मिज़ार चेकर के साथ वितरित किया जाता है और इसे मिज़ार वेबसाइट से स्वतंत्र रूप से डाउनलोड किया जा सकता है। चल रहे एक हालिया प्रोजेक्ट में<ref>[https://archive.today/20130222164311/http://foundations.cs.ru.nl/fndswiki/Research/MathWiki The MathWiki project homepage]</ref> पुस्तकालय को प्रायोगिक [[सप्ताह]] रूप में भी उपलब्ध कराया गया था<ref name="MML wiki">[https://web.archive.org/web/20131202235227/http://mws.cs.ru.nl/mwiki/ The MML in wiki form]</ref> यह केवल तभी संपादनों को स्वीकार करता है जब उन्हें मिज़ार चेकर द्वारा अनुमोदित किया जाता है।<ref>{{cite journal | last = Alama | first = Jesse |author2=Kasper Brink |author3=Lionel Mamane |author4=Josef Urban | title = Large Formal Wikis: Issues and Solutions | journal = Intelligent Computer Mathematics | year = 2011 | volume = 6824 | series = Lecture Notes in Computer Science | pages = 133–148 | doi=10.1007/978-3-642-22673-1_10| arxiv=1107.3212 | isbn = 978-3-642-22672-4 }}</ref>
सभी एमएमएल लेख औपचारिक गणित जर्नल के पेपर के रूप में [[पीडीएफ]] फॉर्म में उपलब्ध हैं।<ref name="Journal of Formalized Mathematics"/> एमएमएल का पूरा पाठ मिज़ार चेकर के साथ वितरित किया जाता है और इसे मिज़ार वेबसाइट से स्वतंत्र रूप से डाउनलोड किया जा सकता है। चल रहे एक हालिया प्रोजेक्ट में<ref>[https://archive.today/20130222164311/http://foundations.cs.ru.nl/fndswiki/Research/MathWiki The MathWiki project homepage]</ref> पुस्तकालय को प्रायोगिक [[सप्ताह]] रूप में भी उपलब्ध कराया गया था<ref name="MML wiki">[https://web.archive.org/web/20131202235227/http://mws.cs.ru.nl/mwiki/ The MML in wiki form]</ref> यह केवल तभी संपादनों को स्वीकार करता है जब उन्हें मिज़ार चेकर द्वारा अनुमोदित किया जाता है।<ref>{{cite journal | last = Alama | first = Jesse |author2=Kasper Brink |author3=Lionel Mamane |author4=Josef Urban | title = Large Formal Wikis: Issues and Solutions | journal = Intelligent Computer Mathematics | year = 2011 | volume = 6824 | series = Lecture Notes in Computer Science | pages = 133–148 | doi=10.1007/978-3-642-22673-1_10| arxiv=1107.3212 | isbn = 978-3-642-22672-4 }}</ref>
एमएमएल क्वेरी वेबसाइट<ref name="MML Query"/>एमएमएल की सामग्री के लिए एक शक्तिशाली खोज इंजन लागू करता है। अन्य क्षमताओं के अलावा, यह किसी विशेष प्रकार या ऑपरेटर के बारे में सिद्ध किए गए सभी एमएमएल प्रमेयों को पुनः प्राप्त कर सकता है।<ref>[http://mmlquery.mizar.org/cgi-bin/mmlquery/emacs_search?input=(symbol+to_power+|+notation+|+constructor+|+occur+|+th)+ordered+by+number+of+ref 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.</ref><ref>[http://mmlquery.mizar.org/cgi-bin/mmlquery/emacs_search?input=(atleast+*+(+PROB_1:modenot+3+ref)+%7C+th)+ordered+by+number+of+ref Another example of an MML query], yielding all theorems proved on [[sigma field]]s.</ref>
 
एमएमएल क्वेरी वेबसाइट<ref name="MML Query" /> एमएमएल की सामग्री के लिए एक शक्तिशाली खोज इंजन प्रयुक्त करता है। अन्य क्षमताओं के अतिरिक्त, यह किसी विशेष प्रकार या ऑपरेटर के बारे में सिद्ध किए गए सभी एमएमएल प्रमेयों को पुनः प्राप्त कर सकता है।<ref>[http://mmlquery.mizar.org/cgi-bin/mmlquery/emacs_search?input=(symbol+to_power+|+notation+|+constructor+|+occur+|+th)+ordered+by+number+of+ref 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.</ref><ref>[http://mmlquery.mizar.org/cgi-bin/mmlquery/emacs_search?input=(atleast+*+(+PROB_1:modenot+3+ref)+%7C+th)+ordered+by+number+of+ref Another example of an MML query], yielding all theorems proved on [[sigma field]]s.</ref>
 




=== तार्किक संरचना ===
=== तार्किक संरचना ===


एमएमएल टार्स्की-ग्रोथेंडिक सेट सिद्धांत के सिद्धांतों पर बनाया गया है। सेट सिद्धांत में गणित के शब्दार्थ कार्यान्वयन के बावजूद, भाषा किसी को [[कमजोर टाइपिंग]] को परिभाषित करने और उपयोग करने की अनुमति देती है। उदाहरण के लिए, किसी सेट को नेट प्रकार का तभी घोषित किया जा सकता है जब उसकी आंतरिक संरचना आवश्यकताओं की एक विशेष सूची के अनुरूप हो। बदले में, यह सूची [[प्राकृतिक संख्या]]ओं की परिभाषा के रूप में कार्य करती है और इस सूची के अनुरूप सभी सेटों के सेट को NAT के रूप में दर्शाया जाता है।<ref>{{cite journal | last = Grabowski | first = Adam |author2=Artur Kornilowicz |author3=Adam Naumowicz  | title = संक्षेप में बढ़ई| journal = [[Journal of Formalized Reasoning]] | year = 2010 | volume = 3 | issue = 2 | pages = 152–245 | url = http://jfr.unibo.it/article/view/1980}}</ref> प्रकारों का यह कार्यान्वयन अधिकांश गणितज्ञों द्वारा प्रतीकों के बारे में औपचारिक रूप से सोचने के तरीके को प्रतिबिंबित करना चाहता है<ref>{{cite book | last = Taylor | first = Paul | title = गणित की व्यावहारिक नींव| year = 1999 | publisher = [[Cambridge University Press]] | isbn = 9780521631075 | url = http://www.cs.man.ac.uk/~pt/Practical-Foundations/html/ | access-date = 2012-07-24 | archive-url = https://web.archive.org/web/20150623031212/http://www.cs.man.ac.uk/~pt/Practical-Foundations/html/ | archive-date = 2015-06-23 | url-status = dead }}</ref> और इसलिए संहिताकरण को सुव्यवस्थित करें।
एमएमएल टार्स्की-ग्रोथेंडिक सेट सिद्धांत के सिद्धांतों पर बनाया गया है। सेट सिद्धांत में गणित के शब्दार्थ कार्यान्वयन के अतिरिक्त, भाषा किसी को [[कमजोर टाइपिंग]] को परिभाषित करने और उपयोग करने की अनुमति देती है। उदाहरण के लिए, किसी सेट को नेट प्रकार का तभी घोषित किया जा सकता है जब उसकी आंतरिक संरचना आवश्यकताओं की एक विशेष सूची के अनुरूप हो। बदले में, यह सूची [[प्राकृतिक संख्या]]ओं की परिभाषा के रूप में कार्य करती है और इस सूची के अनुरूप सभी सेटों के सेट को NAT के रूप में दर्शाया जाता है।<ref>{{cite journal | last = Grabowski | first = Adam |author2=Artur Kornilowicz |author3=Adam Naumowicz  | title = संक्षेप में बढ़ई| journal = [[Journal of Formalized Reasoning]] | year = 2010 | volume = 3 | issue = 2 | pages = 152–245 | url = http://jfr.unibo.it/article/view/1980}}</ref> प्रकारों का यह कार्यान्वयन अधिकांश गणितज्ञों द्वारा प्रतीकों के बारे में औपचारिक रूप से सोचने के विधियों को प्रतिबिंबित करना चाहता है<ref>{{cite book | last = Taylor | first = Paul | title = गणित की व्यावहारिक नींव| year = 1999 | publisher = [[Cambridge University Press]] | isbn = 9780521631075 | url = http://www.cs.man.ac.uk/~pt/Practical-Foundations/html/ | access-date = 2012-07-24 | archive-url = https://web.archive.org/web/20150623031212/http://www.cs.man.ac.uk/~pt/Practical-Foundations/html/ | archive-date = 2015-06-23 | url-status = dead }}</ref> और इसलिए संहिताकरण को सुव्यवस्थित करें।


== मिज़ार प्रूफ चेकर ==
== मिज़ार प्रूफ चेकर ==


सभी प्रमुख ऑपरेटिंग सिस्टम के लिए मिज़ार प्रूफ़ चेकर के वितरण मिज़ार प्रोजेक्ट वेबसाइट पर डाउनलोड के लिए निःशुल्क उपलब्ध हैं। प्रूफ चेकर का उपयोग सभी गैर-व्यावसायिक उद्देश्यों के लिए निःशुल्क है। यह [[ मुफ़्त पास्कल ]] में लिखा गया है और स्रोत कोड मिज़ार उपयोगकर्ताओं के संघ के सभी सदस्यों के लिए उपलब्ध है।<ref name="The Association of Mizar Users website">[http://mizar.uwb.edu.pl/sum/ The Association of Mizar Users website]</ref>
सभी प्रमुख ऑपरेटिंग प्रणाली के लिए मिज़ार प्रूफ़ चेकर के वितरण मिज़ार प्रोजेक्ट वेबसाइट पर डाउनलोड के लिए निःशुल्क उपलब्ध हैं। प्रूफ चेकर का उपयोग सभी गैर-व्यावसायिक उद्देश्यों के लिए निःशुल्क है। यह [[ मुफ़्त पास्कल ]] में लिखा गया है और स्रोत कोड मिज़ार उपयोगकर्ताओं के संघ के सभी सदस्यों के लिए उपलब्ध है।<ref name="The Association of Mizar Users website">[http://mizar.uwb.edu.pl/sum/ The Association of Mizar Users website]</ref>




Revision as of 09:21, 21 July 2023

For तारा प्रणाली, see मिज़ार (स्टार).
Mizar
File:Mizar system logo.gif
Screenshot
Mizar MathWiki screenshot.png
Mizar MathWiki screenshot
ParadigmDeclarative
द्वारा डिज़ाइन किया गया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]


मिज़ार गणितीय पुस्तकालय

मिज़ार गणितीय लाइब्रेरी (MML) में सभी प्रमेय सम्मिलित हैं जिनका लेखक नए लिखे गए लेखों में उल्लेख कर सकते हैं। एक बार प्रमाण जांचकर्ता द्वारा अनुमोदित किए जाने के बाद उचित योगदान और शैली के लिए सहकर्मी-समीक्षा की प्रक्रिया में उनका आगे मूल्यांकन किया जाता है। यदि स्वीकार कर लिया जाता है तो उन्हें एसोसिएटेड जर्नल ऑफ फॉर्मलाइज्ड मैथमेटिक्स में प्रकाशित किया जाता है[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. ↑ 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. ↑ 2.0 2.1 Wiedijk, Freek (2009). "एरो के प्रमेय को औपचारिक बनाना". Sādhanā. 34 (1): 193–220. doi:10.1007/s12046-009-0005-1. hdl:2066/75428.
  3. ↑ Matuszewski, Roman; Piotr Rudnicki (2005). "Mizar: the first 30 years" (PDF). Mechanized Mathematics and Its Applications. 4.
  4. ↑ Wiedijk, Freek. "बढ़ई". Retrieved 24 July 2018.
  5. ↑ Mailing list discussion Archived 2011-10-09 at the Wayback Machine referring to the close-sourcing of Mizar.
  6. ↑ Mailing list announcement referring to the open-sourcing of MML.
  7. ↑ Geuvers, H. (2009). "Proof assistants: History, ideas and future". Sādhanā. 34 (1): 3–25. doi:10.1007/s12046-009-0001-5.
  8. ↑ Wiedijk, Freek (2008). "औपचारिक प्रमाण--आरंभ करना" (PDF). Notices of the AMS. 55 (11): 1408–1414.
  9. ↑ Wiedijk, Freek. ""डी ब्रुइज़न फ़ैक्टर"". Retrieved 24 July 2018.
  10. ↑ 10.0 10.1 Journal of Formalized Mathematics
  11. ↑ 11.0 11.1 The MML Query search engine
  12. ↑ "एमएमएल में नामित प्रमेयों की एक सूची". Retrieved 22 July 2012.
  13. ↑ Wiedijk, Freek (2007). "QED घोषणापत्र पर दोबारा गौर किया गया". From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric. 10 (23).
  14. ↑ The MathWiki project homepage
  15. ↑ The MML in wiki form
  16. ↑ 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.
  17. ↑ 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.
  18. ↑ Another example of an MML query, yielding all theorems proved on sigma fields.
  19. ↑ Grabowski, Adam; Artur Kornilowicz; Adam Naumowicz (2010). "संक्षेप में बढ़ई". Journal of Formalized Reasoning. 3 (2): 152–245.
  20. ↑ Taylor, Paul (1999). गणित की व्यावहारिक नींव. Cambridge University Press. ISBN 9780521631075. Archived from the original on 2015-06-23. Retrieved 2012-07-24.
  21. ↑ The Association of Mizar Users website


बाहरी संबंध

Retrieved from ‘https://www.vigyanwiki.in/index.php?title=मिज़ार_प्रणाली&oldid=235228’