मेटामैथ

From Vigyanwiki
Revision as of 06:50, 2 June 2023 by alpha>Indicwiki (Created page with "{{Short description|Formal language and associated computer program}} {{For|the study of mathematics using mathematical methods|Metamathematics}} {{Infobox software |name = Me...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
For the study of mathematics using mathematical methods, see Metamathematics.
Metamath
Developer(s)Norman Megill
Initial release0.07 in June 2005; 19 years ago (2005-06)
Stable release
Script error: The module returned a nil value. It is supposed to return an export table. / Script error: The module returned a nil value. It is supposed to return an export table.; Error: first parameter cannot be parsed as a date or time. (Script error: The module returned a nil value. It is supposed to return an export table.)
Written inANSI C
Operating systemLinux, Windows, macOS
TypeComputer-assisted proof checking
LicenseGNU General Public License (Creative Commons Public Domain Dedication for databases)
Websitemetamath.org

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

As of February 2022, मेटामैथ का उपयोग करके सिद्ध प्रमेय का सेट औपचारिक गणित के सबसे बड़े निकायों में से एक है, जिसमें 74 के विशेष प्रमाण शामिल हैं[3] औपचारिक 100 प्रमेय चुनौती के 100 प्रमेयों में से,[4] एचओएल लाइट, इसाबेल (सबूत सहायक) और कोक के बाद चौथे स्थान पर रही, लेकिन मिज़ार प्रणाली , प्रूफ पावर , लीन (सबूत सहायक) , एनकथम, ACL2 और एनयूपीआरएल से पहले। मेटामैथ प्रारूप का उपयोग करने वाले डेटाबेस के लिए कम से कम 19 प्रमाण सत्यापनकर्ता हैं।[5] यह परियोजना अपनी तरह की पहली परियोजना है जो एक साधारण वेबसाइट के रूप में अपने औपचारिक प्रमेय डेटाबेस के इंटरैक्टिव ब्राउज़िंग की अनुमति देती है।[6]


मेटामथ भाषा

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

मेटामैथ भाषा डिजाइन सादगी पर केंद्रित है; परिभाषाओं, स्वयंसिद्धों, अनुमान नियमों और प्रमेयों को बताने के लिए नियोजित भाषा केवल कुछ मुट्ठी भर खोजशब्दों से बनी होती है, और चर के प्रतिस्थापन के आधार पर एक सरल एल्गोरिथ्म का उपयोग करके सभी प्रमाणों की जाँच की जाती है (वैकल्पिक प्रावधानों के साथ कि किस चर को अलग रहना चाहिए) प्रतिस्थापन के बाद)।[7]


भाषा की मूल बातें

सूत्रों के निर्माण के लिए उपयोग किए जा सकने वाले प्रतीकों का सेट उपयोग करके घोषित किया जाता है $c (निरंतर प्रतीक) और $v (चर प्रतीक) कथन; उदाहरण के लिए:

<पूर्व> $( उन स्थिर प्रतीकों की घोषणा करें जिनका हम उपयोग करेंगे $) 

   $c 0 + = -> ( ) शब्द wff |- $.

$( उन मेटावेरिएबल्स की घोषणा करें जिनका हम $ उपयोग करेंगे) 

   $v t r s P Q $।

</पूर्व>

सूत्रों के लिए व्याकरण के संयोजन का उपयोग करके निर्दिष्ट किया गया है $f (फ्लोटिंग (वैरिएबल-टाइप) परिकल्पना) और $a (स्वयंसिद्ध अभिकथन) कथन; उदाहरण के लिए:

<पूर्व> $( मेटावेरिएबल्स के गुण निर्दिष्ट करें $) 

   टीटी $ च अवधि टी $।
   tr $f अवधि r $।
   टीएस $ च अवधि एस $।
   डब्ल्यूपी $एफ डब्ल्यूएफएफ पी $।
   wq $f wff क्यू $।

$(wff परिभाषित करें (भाग 1) $) 

   Weq $a wff t = r $.

$(wff परिभाषित करें (भाग 2) $) 

   wim $a wff ( P -> Q ) $.

</पूर्व>

अभिगृहीतों और अनुमान के नियमों को निर्दिष्ट किया गया है $a साथ में बयान ${ और $} ब्लॉक स्कूपिंग और वैकल्पिक के लिए $e (आवश्यक परिकल्पना) कथन; उदाहरण के लिए:

<पूर्व> $(राज्य स्वयंसिद्ध a1 $) 

   a1 $a |- (t = r -> (t = s -> r = s)) $।

$(राज्य स्वयंसिद्ध a2 $) 

   a2 $a |- (t + 0) = t $।
   ${
      मिन $ई |-पी $।
      माज $ई |- (पी -> क्यू) $।

$(मॉडस पोनेन्स इंट्रेंस रूल को परिभाषित करें $) 

      एमपी $ ए |- क्यू $।
   $}

</पूर्व>

एक निर्माण का उपयोग करना, $a कथन, सिंटैक्टिक नियमों, स्वयंसिद्ध स्कीमाओं और अनुमान के नियमों को पकड़ने के लिए एक जटिल प्रकार की प्रणाली पर निर्भरता के बिना LF (तार्किक ढांचे) के समान लचीलेपन का स्तर प्रदान करने का इरादा है।

प्रमाण

प्रमेय (और अनुमान के व्युत्पन्न नियम) के साथ लिखे गए हैं $p कथन; उदाहरण के लिए:

<पूर्व> $(एक प्रमेय $ साबित करें) 

   th1 $p |- t = t $=
 $(यहाँ इसका प्रमाण है: $)
      tt tze tpl tt weq tt tt weq tt a2 tt tze tpl
      tt weq tt tze tpl tt weq tt tt weq wim tt a2
      tt tze tpl tt tt a1 mp mp
    $।

</पूर्व>

में प्रमाण को शामिल करने पर ध्यान दें $p कथन। यह निम्नलिखित विस्तृत प्रमाण को संक्षिप्त करता है: 

tt            $f term t
tze           $a term 0
1,2 tpl       $a term ( t + 0 )
3,1 weq       $a wff ( t + 0 ) = t
1,1 weq       $a wff t = t
1 a2          $a |- ( t + 0 ) = t
1,2 tpl       $a term ( t + 0 )
7,1 weq       $a wff ( t + 0 ) = t
1,2 tpl       $a term ( t + 0 )
9,1 weq       $a wff ( t + 0 ) = t
1,1 weq       $a wff t = t
10,11 wim     $a wff ( ( t + 0 ) = t -> t = t )
1 a2          $a |- ( t + 0 ) = t
1,2 tpl       $a term ( t + 0 )
14,1,1 a1     $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )
8,12,13,15 mp $a |- ( ( t + 0 ) = t -> t = t )
4,5,6,16 mp   $a |- t = t

सबूत का आवश्यक रूप एक अधिक परंपरागत प्रस्तुति छोड़कर, वाक्यात्मक विवरण को समाप्त करता है: 

a2             $a |- ( t + 0 ) = t
a2             $a |- ( t + 0 ) = t
a1             $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )
2,3 mp         $a |- ( ( t + 0 ) = t -> t = t )
1,4 mp         $a |- t = t


प्रतिस्थापन

चरण-दर-चरण प्रमाण

सभी मेटामैथ प्रूफ स्टेप्स एक एकल प्रतिस्थापन नियम का उपयोग करते हैं, जो एक अभिव्यक्ति के साथ एक चर का सरल प्रतिस्थापन है और विधेय कलन पर काम में वर्णित उचित प्रतिस्थापन नहीं है। मेटामैथ डेटाबेस में इसका समर्थन करने वाले उचित प्रतिस्थापन, मेटामैथ भाषा में निर्मित एक के बजाय एक व्युत्पन्न निर्माण है।

प्रतिस्थापन नियम उपयोग में तर्क प्रणाली के बारे में कोई धारणा नहीं बनाता है और केवल यह आवश्यक है कि चर के प्रतिस्थापन सही तरीके से किए जाएं।

यह एल्गोरिदम कैसे काम करता है इसका एक विस्तृत उदाहरण यहां दिया गया है। प्रमेय के चरण 1 और 2 2p2e4 मेटामैथ प्रूफ एक्सप्लोरर (set.mm) में बाईं ओर दर्शाया गया है। आइए बताते हैं कि जब आप प्रमेय का उपयोग करते हैं तो चरण 2 चरण 1 का तार्किक परिणाम है, यह जांचने के लिए मेटामैथ अपने प्रतिस्थापन एल्गोरिथ्म का उपयोग कैसे करता है opreq2i. चरण 2 बताता है कि ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ). यह प्रमेय का निष्कर्ष है opreq2i. प्रमेय opreq2i बताता है कि अगर A = B, तब (C F A) = (C F B). यह प्रमेय किसी पाठ्यपुस्तक में इस गूढ़ रूप में कभी प्रकट नहीं होगा, लेकिन इसका साक्षर सूत्रीकरण साधारण है: जब दो मात्राएँ समान होती हैं, तो एक संक्रिया में एक के बाद एक को प्रतिस्थापित किया जा सकता है। सबूत की जांच करने के लिए मेटामैथ एकजुट होने का प्रयास करता है (C F A) = (C F B) साथ ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ). ऐसा करने का एक ही तरीका है: एकता C साथ 2, F साथ +, A साथ 2 और B साथ ( 1 + 1 ). तो अब मेटामैथ के आधार का उपयोग करता है opreq2i. यह प्रमेय बताता है कि A = B. अपनी पिछली संगणना के परिणामस्वरूप, मेटामैथ यह जानता है A द्वारा प्रतिस्थापित किया जाना चाहिए 2 और B द्वारा ( 1 + 1 ). परिसर A = B हो जाता है 2=( 1 + 1 ) और इस प्रकार चरण 1 उत्पन्न होता है। इसके बदले में चरण 1 एकीकृत है df-2. df-2 संख्या की परिभाषा है 2 और बताता है कि 2 = ( 1 + 1 ). यहाँ एकीकरण केवल स्थिरांक का मामला है और सीधा है (स्थानापन्न करने के लिए चर की कोई समस्या नहीं है)। तो सत्यापन समाप्त हो गया है और प्रमाण के ये दो चरण हैं 2p2e4 सही हैं।

जब मेटामैथ एकीकृत होता है ( 2 + 2 ) साथ B यह जांचना है कि वाक्य-विन्यास के नियमों का सम्मान किया जाता है। वास्तव में B का प्रकार है class इस प्रकार मेटामैथ को इसकी जांच करनी है ( 2 + 2 ) भी टाइप किया गया है class.

मेटामैथ प्रूफ चेकर

मेटामैथ प्रोग्राम मेटामैथ भाषा का उपयोग करके लिखे गए डेटाबेस में हेरफेर करने के लिए बनाया गया मूल प्रोग्राम है। इसमें एक टेक्स्ट (कमांड लाइन) इंटरफेस है और इसे सी में लिखा गया है। यह मेटामैथ डेटाबेस को मेमोरी में पढ़ सकता है, डेटाबेस के प्रूफ को सत्यापित कर सकता है, डेटाबेस को संशोधित कर सकता है (विशेष रूप से प्रूफ जोड़कर), और उन्हें स्टोरेज में वापस लिख सकता है।

इसमें एक सिद्ध कमांड है जो उपयोगकर्ताओं को मौजूदा प्रमाणों की खोज के लिए तंत्र के साथ-साथ एक प्रमाण दर्ज करने में सक्षम बनाता है।

मेटामैथ प्रोग्राम स्टेटमेंट को HTML या TeX नोटेशन में बदल सकता है; उदाहरण के लिए, यह set.mm से modus ponens axiom को आउटपुट कर सकता है:

कई अन्य प्रोग्राम मेटामैथ डेटाबेस को संसाधित कर सकते हैं, विशेष रूप से, मेटामैथ प्रारूप का उपयोग करने वाले डेटाबेस के लिए कम से कम 19 प्रूफ सत्यापनकर्ता हैं।[8]


मेटामैथ डेटाबेस

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

मेटामैथ प्रूफ एक्सप्लोरर

Metamath Proof Explorer
File:Metamath-theorem-avril1-indexed.png
A proof of the Metamath Proof Explorer
साइट का प्रकार
Online encyclopedia
HeadquartersUSA
मालिकNorman Megill
के द्वारा बनाई गईNorman Megill
यूआरएलus.metamath.org/mpeuni/mmset.html
व्यावसायिकNo
पंजीकरणNo

मेटामैथ प्रूफ एक्सप्लोरर (set.mm में रिकॉर्ड किया गया) मुख्य और अब तक का सबसे बड़ा डेटाबेस है, जिसके जुलाई 2019 तक इसके मुख्य भाग में 23,000 से अधिक प्रूफ हैं। यह शास्त्रीय प्रथम-क्रम तर्क और ZFC सेट सिद्धांत पर आधारित है (साथ में) जरूरत पड़ने पर टार्स्की-ग्रोथेंडिक सेट थ्योरी को जोड़ना, उदाहरण के लिए श्रेणी सिद्धांत में)। डेटाबेस को बीस वर्षों से अधिक समय तक बनाए रखा गया है (सेट.एमएम में पहला प्रमाण अगस्त 1993 का है)। डेटाबेस में अन्य क्षेत्रों के बीच, सेट थ्योरी (ऑर्डिनल्स और कार्डिनल्स, रिकर्सन, पसंद के स्वयंसिद्ध के समकक्ष, सातत्य परिकल्पना ...), वास्तविक और जटिल संख्या प्रणालियों का निर्माण, ऑर्डर थ्योरी, ग्राफ थ्योरी, के विकास शामिल हैं। सार बीजगणित, रैखिक बीजगणित, सामान्य टोपोलॉजी, वास्तविक और जटिल विश्लेषण, हिल्बर्ट रिक्त स्थान, संख्या सिद्धांत और प्राथमिक ज्यामिति। यह डेटाबेस पहले नॉर्मन मेगिल द्वारा बनाया गया था, लेकिन 2019-10-04 तक इसमें 48 योगदानकर्ता (नॉर्मन मेगिल सहित) रहे हैं।[9] मेटामैथ प्रूफ एक्सप्लोरर कई पाठ्य पुस्तकों का संदर्भ देता है जिनका उपयोग मेटामैथ के संयोजन में किया जा सकता है।[10] इस प्रकार, गणित के अध्ययन में रुचि रखने वाले लोग इन पुस्तकों के संबंध में मेटामैथ का उपयोग कर सकते हैं और यह सत्यापित कर सकते हैं कि सिद्ध कथन साहित्य से मेल खाते हैं।

अंतर्ज्ञानवादी तर्क एक्सप्लोरर

यह डेटाबेस एक रचनात्मक दृष्टिकोण से गणित को विकसित करता है, अंतर्ज्ञानवादी तर्क के सिद्धांतों से शुरू होता है और रचनात्मक सेट सिद्धांत के स्वयंसिद्ध प्रणालियों के साथ जारी रहता है।

नई नींव एक्सप्लोरर

यह डेटाबेस Quine's New Foundations set Theory से गणित विकसित करता है।

उच्च क्रम तर्क एक्सप्लोरर

यह डेटाबेस उच्च-क्रम तर्क के साथ शुरू होता है और प्रथम-क्रम तर्क और ZFC सेट सिद्धांत के स्वयंसिद्धों के समकक्ष प्राप्त करता है।

खोजकर्ता के बिना डेटाबेस

मेटामैथ वेबसाइट कुछ अन्य डेटाबेस को होस्ट करती है जो खोजकर्ताओं से संबद्ध नहीं हैं लेकिन फिर भी उल्लेखनीय हैं। रॉबर्ट सोलोवे द्वारा लिखित डेटाबेस पीनो.एमएम पियानो अंकगणित को औपचारिक रूप देता है। डेटाबेस nat.mm[11] प्राकृतिक कटौती को औपचारिक रूप देता है। डेटाबेस miu.mm Gödel, Escher, Bach में प्रस्तुत औपचारिक प्रणाली MIU के आधार पर MU पहेली को औपचारिक रूप देता है।

पुराने खोजकर्ता

मेटामैथ वेबसाइट कुछ पुराने डेटाबेस को भी होस्ट करती है जो अब बनाए नहीं रखे जाते हैं, जैसे कि हिल्बर्ट स्पेस एक्सप्लोरर, जो हिल्बर्ट अंतरिक्ष सिद्धांत से संबंधित प्रमेय प्रस्तुत करता है जिसे अब मेटामैथ प्रूफ एक्सप्लोरर में विलय कर दिया गया है, और क्वांटम तर्क एक्सप्लोरर, जो क्वांटम विकसित करता है ऑर्थोमॉड्यूलर लैटिस के सिद्धांत से शुरू होने वाला तर्क।

प्राकृतिक कटौती

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

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

==मेटामैथ== से जुड़े अन्य कार्य

प्रूफ चेकर्स

मेटामैथ में लागू किए गए डिजाइन विचारों का उपयोग करते हुए, राफ लेविन ने पायथन कोड की केवल 500 लाइनों पर बहुत छोटे प्रूफ चेकर, mmverify.py को लागू किया है।

Ghilbert mmverify.py पर आधारित समान यद्यपि अधिक विस्तृत भाषा है।[12] लेविन एक ऐसी प्रणाली को लागू करना चाहते हैं जहां कई लोग सहयोग कर सकें और उनका काम मॉड्यूलरिटी और छोटे सिद्धांतों के बीच संबंध पर जोर दे रहा है।

लेविएन मौलिक कार्यों का उपयोग करते हुए, मेटामैथ डिजाइन सिद्धांतों के कई अन्य कार्यान्वयन विभिन्न प्रकार की भाषाओं के लिए लागू किए गए हैं। Juha Arpiainen ने सामान्य लिस्प में Bourbaki नामक अपना स्वयं का प्रूफ़ चेकर कार्यान्वित किया है[13] और Marnix Klooster ने Hmm नामक हास्केल (प्रोग्रामिंग भाषा) में एक प्रूफ चेकर को कोडित किया है।[14] हालांकि वे सभी औपचारिक सिस्टम चेकर कोडिंग के लिए समग्र मेटामैथ दृष्टिकोण का उपयोग करते हैं, वे स्वयं की नई अवधारणाओं को भी लागू करते हैं।

संपादक

Mel O'Cat ने Mmj2 नामक एक सिस्टम डिज़ाइन किया है, जो प्रूफ एंट्री के लिए ग्राफिक यूजर इंटरफेस प्रदान करता है।[15] मेल ओ'काट का प्रारंभिक उद्देश्य उपयोगकर्ता को केवल सूत्रों को टाइप करके सबूत दर्ज करने की अनुमति देना था और Mmj2 को उन्हें जोड़ने के लिए उपयुक्त अनुमान नियम खोजने देना था। इसके विपरीत मेटामैथ में आप केवल प्रमेयों के नाम दर्ज कर सकते हैं। आप सीधे सूत्र दर्ज नहीं कर सकते हैं। Mmj2 में प्रूफ को आगे या पीछे प्रवेश करने की भी संभावना है (मेटामथ केवल प्रूफ बैकवर्ड में प्रवेश करने की अनुमति देता है)। इसके अलावा एमएमजे 2 में वास्तविक व्याकरण पार्सर है (मेटामैथ के विपरीत)। यह तकनीकी अंतर उपयोगकर्ता को अधिक सुविधा प्रदान करता है। विशेष रूप से मेटामैथ कभी-कभी कई सूत्रों के बीच झिझकता है जो इसका विश्लेषण करता है (उनमें से अधिकतर व्यर्थ हैं) और उपयोगकर्ता को चुनने के लिए कहता है। Mmj2 में यह सीमा अब मौजूद नहीं है।

मेटामैथ में एममाइड नामक एक ग्राफिकल यूजर इंटरफेस जोड़ने के लिए विलियम हेल द्वारा एक परियोजना भी है।[16] पॉल चैपमैन अपनी बारी में एक नए प्रूफ ब्राउज़र पर काम कर रहे हैं, जिसमें हाइलाइटिंग है जो आपको प्रतिस्थापन के पहले और बाद में संदर्भित प्रमेय को देखने की अनुमति देता है।

मिलपगेम एक प्रूफ असिस्टेंट और एक चेकर है (यह एक संदेश दिखाता है कि कुछ गलत हो गया है) मेटामैथ लैंग्वेज (सेट.एमएम) के लिए एक ग्राफिक यूजर इंटरफेस के साथ, फिलिप सेर्नाटेस्कू द्वारा लिखा गया है, यह एक ओपन सोर्स (एमआईटी लाइसेंस) जावा एप्लिकेशन है ( क्रॉस-प्लेटफ़ॉर्म एप्लिकेशन: विंडो, लिनक्स, मैक ओएस)। उपयोगकर्ता दो तरीकों से प्रदर्शन (प्रमाण) में प्रवेश कर सकता है: साबित करने के लिए कथन के सापेक्ष आगे और पीछे। Milpgame जाँचता है कि क्या कोई कथन अच्छी तरह से बना है (एक वाक्यात्मक सत्यापनकर्ता है)। यह डमीलिंक प्रमेय के उपयोग के बिना अधूरे प्रमाणों को सहेज सकता है। प्रदर्शन को पेड़ के रूप में दिखाया गया है, बयानों को html परिभाषाओं (टाइपसेटिंग अध्याय में परिभाषित) का उपयोग करके दिखाया गया है। Milpgame को Java .jar (JRE संस्करण 6 अपडेट 24 NetBeans IDE में लिखा गया है) के रूप में वितरित किया गया है।

यह भी देखें

संदर्भ

  1. ↑ Megill, Norman; Wheeler, David A. (2019-06-02). Metamath: A Computer Language for Mathematical Proofs (Second ed.). Morrisville, North Carolina, US: Lulul Press. p. 248. ISBN 978-0-359-70223-7.
  2. ↑ Megill, Norman. "What is Metamath?". Metamath Home Page.
  3. ↑ Metamath 100.
  4. ↑ "Formalizing 100 Theorems".
  5. ↑ Megill, Norman. "ज्ञात मेटामैथ प्रूफ सत्यापनकर्ता". Retrieved 8 October 2022.
  6. ↑ TOC of Theorem List - Metamath Proof Explorer
  7. ↑ Megill,Norman. "सबूत कैसे काम करते हैं". Metamath Proof Explorer Home Page.
  8. ↑ Megill, Norman. "ज्ञात मेटामैथ प्रूफ सत्यापनकर्ता". Retrieved 8 October 2022.
  9. ↑ Wheeler, David A. "Metamath set.mm contributions viewed with Gource through 2019-10-04". YouTube. Archived from the original on 2021-12-19.
  10. ↑ Megill, Norman. "सुझाव पढ़ना". Metamath.
  11. ↑ Liné, Frédéric. "प्राकृतिक कटौती आधारित मेटामैथ प्रणाली". Archived from the original on 2012-12-28.
  12. ↑ Levien,Raph. "गिल्बर्ट".
  13. ↑ Arpiainen, Juha. "बोरबाकी की प्रस्तुति". Archived from the original on 2012-12-28.
  14. ↑ Klooster,Marnix. "हम्म की प्रस्तुति". Archived from the original on 2012-04-02.
  15. ↑ O'Cat,Mel. "Presentation of mmj2". Archived from the original on December 19, 2013.
  16. ↑ Hale, William. "एममाइड की प्रस्तुति". Archived from the original on 2012-12-28.


बाहरी संबंध

Retrieved from ‘https://www.vigyanwiki.in/index.php?title=मेटामैथ&oldid=205632’