View source for मेटामैथ

{{Short description|Formal language and associated computer program}}
{{For|गणितीय विधियों का उपयोग करके गणित का अध्ययन|मेटामैथमैटिक्स}}
{{Infobox software
|name = Metamath
|logo=[[Image:Metamath logo.png|100px]]
|developer = Norman Megill
|released = 0.07 in {{Start date and age|2005|06}}
|programming language   = [[ANSI C]]
|operating_system = [[Linux]], [[Microsoft Windows|Windows]], [[macOS]]
|genre = Computer-assisted proof checking
|license = [[GNU General Public License]] ([[Creative Commons]] [[Public Domain]] Dedication for databases)
|latest release version = {{wikidata|property|edit|reference|P348}}
|latest release date    = {{start date and age|{{wikidata|qualifier|P348|P577}}}}
|website = {{URL|http://metamath.org}}
}}

'''मेटामैथ''' एक [[औपचारिक भाषा]] है और गणितीय प्रमाणों का संग्रह, सत्यापन और अध्ययन करने के लिए एक संबद्ध कंप्यूटर प्रोग्राम (एक [[ सबूत चेकर | प्रमाण जाँचकर्ता]] ) है। <ref name="metamath-book">{{cite book |last1=Megill |first1=Norman |last2=Wheeler |first2=David A. |title=Metamath: A Computer Language for Mathematical Proofs |date=2019-06-02 |publisher=Lulul Press |location=Morrisville, North Carolina, US |isbn=978-0-359-70223-7 |pages=248 |edition= Second |url=http://us.metamath.org/#book}}</ref> सिद्ध प्रमेय के कई आंकड़ाकोष मेटामैथ का उपयोग करके [[तर्क]], सम्मुच्चय सिद्धांत, [[संख्या सिद्धांत]], [[बीजगणित]], [[टोपोलॉजी|सांस्थिति]] और [[गणितीय विश्लेषण]] में मानक परिणामों को सम्मिलित करते हुए विकसित किए गए हैं। <ref>{{cite web | author=Megill, Norman | title=What is Metamath? | work=Metamath Home Page | url=http://us.metamath.org/#faq}}</ref>

{{As of|February 2022}}, मेटामैथ का उपयोग करके सिद्ध प्रमेय का सम्मुच्चय औपचारिक गणित के सबसे बड़े निकायों में से एक है, जिसमें औपचारिक 100 प्रमेय चुनौती के 100 प्रमेयों में से 74 के विशेष प्रमाण सम्मिलित हैं, <ref>[http://us.metamath.org/mm_100.html Metamath 100.]</ref><ref>{{cite web | url=https://www.cs.ru.nl/~freek/100/ | title=Formalizing 100 Theorems }}</ref> एचओएल लाइट, इसाबेल और कॉक के बाद यह चौथे स्थान पर है, लेकिन मिज़ार, प्रमाणपावर, लीन, एनक्यूटीएम, एसीएल2 और नुप्रल से पहले है। मेटामैथ प्रारूप का उपयोग करने वाले आंकड़ाकोष के लिए कम से कम 19 प्रमाण सत्यापनकर्ता हैं। <ref>{{cite web |last1=Megill |first1=Norman |title=ज्ञात मेटामैथ प्रूफ सत्यापनकर्ता|url=http://us.metamath.org/other.html#verifiers |accessdate=8 October 2022}}</ref> यह परियोजना अपनी तरह की पहली परियोजना है जो एक साधारण वेबसाइट के रूप में अपने औपचारिक प्रमेय आंकड़ाकोष के पारस्परिक विचरण की अनुमति देती है। <ref>[http://us2.metamath.org:88/mpeuni/mmtheorems.html TOC of Theorem List - Metamath Proof Explorer]</ref>


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

प्रमाणित प्रमेयों का सबसे बड़ा आंकड़ाकोष पारंपरिक [[ZFC|जेडएफसी]] सम्मुच्चय सिद्धांत और पारम्परिक तर्क का अनुसरण करता है, लेकिन अन्य आंकड़ाकोष उपस्थित हैं और अन्य बनाए जा सकते हैं।

मेटामैथ भाषा अभिकल्पना सादगी पर केंद्रित है; परिभाषाओं, स्वयंसिद्धों, अनुमान नियमों और प्रमेयों को बताने के लिए नियोजित भाषा केवल कुछ मुट्ठी भर खोजशब्दों से बनी होती है, और चर के प्रतिस्थापन के आधार पर एक सरल कलन विधि का उपयोग करके सभी प्रमाणों की जाँच की जाती है (प्रतिस्थापन के बाद कौन से चर अलग रहना चाहिए इसके लिए वैकल्पिक प्रावधानों के साथ)।<ref name="howpswork">{{cite web | author=Megill,Norman | title=सबूत कैसे काम करते हैं| work=Metamath Proof Explorer Home Page | url=http://us.metamath.org/mpegif/mmset.html#proofs}}</ref>



=== भाषा की मूल बातें ===
सूत्रों के निर्माण के लिए उपयोग किए जा सकने वाले प्रतीकों का सम्मुच्चय <code>$c</code> (निरंतर प्रतीक) और <code>$v</code> (चर प्रतीक) कथन उपयोग करके घोषित किया जाता है; उदाहरण के लिए:
 $( Declare the constant symbols we will use $)

     $c 0 + = -> ( ) term wff |- $.

 $( Declare the metavariables we will use $)

     $v t r s P Q $.
सूत्रों के लिए व्याकरण $f (अस्थिर (चर-प्रकार) परिकल्पना) और $a (स्वयंसिद्ध अभिकथन) कथनों के संयोजन का उपयोग करके निर्दिष्ट किया गया है; उदाहरण के लिए:
    $( Specify properties of the metavariables $)

     tt $f term t $.
     tr $f term r $.
     ts $f term s $.
     wp $f wff P $.
     wq $f wff Q $.
 $( Define "wff" (part 1) $)
     weq $a wff t = r $.
 $( Define "wff" (part 2) $)
     wim $a wff ( P -> Q ) $.


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

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

     a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
 $( State axiom a2 $)
     a2 $a |- ( t + 0 ) = t $.
     ${
        min $e |- P $.
        maj $e |- ( P -> Q ) $.
 $( Define the modus ponens inference rule $)
        mp  $a |- Q $.
     $}
एक निर्माण का उपयोग करना, <code>$a</code> कथन, वाक्यात्मक नियमों, स्वयंसिद्ध स्कीमाओं और अनुमान के नियमों को पकड़ने के लिए एक जटिल प्रकार की प्रणाली पर निर्भरता के बिना LF (तार्किक ढांचे) के समान लचीलेपन का स्तर प्रदान करने का अभिप्रेत है।

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

     th1 $p |- t = t $=
   $( Here is its proof: $)
        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
      $.
<code>$p</code> कथन में प्रमाण को सम्मिलित करने पर ध्यान दें। यह निम्नलिखित विस्तृत प्रमाण को संक्षिप्त करता है:

<syntaxhighlight line lang="nasm">
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
</syntaxhighlight>
प्रमाण का आवश्यक रूप एक अधिक परंपरागत प्रस्तुति छोड़कर, वाक्यात्मक विवरण को समाप्त करता है:

<syntaxhighlight line lang="nasm">
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
</syntaxhighlight>


=== प्रतिस्थापन ===
[[Image:Proofstep.gif|thumb|right|592px|चरण-दर-चरण प्रमाण]]सभी मेटामैथ प्रमाण चरण एक एकल प्रतिस्थापन नियम का उपयोग करते हैं, जो एक अभिव्यक्ति के साथ एक चर का सरल प्रतिस्थापन है और विधेय कलन पर काम में वर्णित उचित प्रतिस्थापन नहीं है। मेटामैथ आंकड़ाकोष में इसका समर्थन करने वाले उचित प्रतिस्थापन, मेटामैथ भाषा में निर्मित एक के स्थान पर एक व्युत्पन्न निर्माण है।

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

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

जब मेटामैथ {{math|1=( 2 + 2 )}} के साथ {{magenta|{{mvar|B}}}} एकीकृत होता है।  यह जांचना है कि वाक्य-विन्यास के नियमों का सम्मान किया जाता है। वास्तव में {{magenta|{{mvar|B}}}} में टाइप <code>class</code> है इसलिए मेटामैथ को यह जांचना होगा कि (2 + 2) भी टाइप <code>class</code> है।

== मेटामैथ प्रमाण जाँचकर्ता ==
मेटामैथ प्रोग्राम मेटामैथ भाषा का उपयोग करके लिखे गए आंकड़ाकोष में हस्त कौशल करने के लिए बनाया गया मूल प्रोग्राम है। इसमें एक पाठ (कमांड लाइन) अंतरापृष्ठ है और इसे C में लिखा गया है। यह मेटामैथ आंकड़ाकोष को मेमोरी में पढ़ सकता है, आंकड़ाकोष के प्रमाण को सत्यापित कर सकता है, आंकड़ाकोष को संशोधित कर सकता है (विशेष रूप से प्रमाण जोड़कर), और उन्हें स्टोरेज में वापस लिख सकता है।

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

मेटामैथ प्रोग्राम वर्णन को [[HTML|एचटीएमएल]] या टीईएक्स संकेत पद्धति में बदल सकता है;

उदाहरण के लिए, यह एसईटी.एमएम से [[modus ponens|विधानात्मक हेतुफलानुमान]] सूक्ति को प्रक्षेपण कर सकता है:

:<math>\vdash \varphi\quad\&\quad \vdash ( \varphi \rightarrow \psi )\quad\Rightarrow\quad \vdash \psi</math>
कई अन्य प्रोग्राम मेटामैथ आंकड़ाकोष को संसाधित कर सकते हैं, विशेष रूप से, मेटामैथ प्रारूप का उपयोग करने वाले आंकड़ाकोष के लिए कम से कम 19 प्रमाण सत्यापनकर्ता हैं। <ref>{{cite web |last1=Megill |first1=Norman |title=ज्ञात मेटामैथ प्रूफ सत्यापनकर्ता|url=http://us.metamath.org/other.html#verifiers |accessdate=8 October 2022}}</ref>



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

=== मेटामैथ प्रमाण अन्वेषक ===
{{Infobox website
| name = Metamath Proof Explorer
|screenshot = [[Image:Metamath-theorem-avril1-indexed.png|280px]]
|caption = ''A proof of the Metamath Proof Explorer''
| url = {{URL|http://us.metamath.org/mpeuni/mmset.html}}
| commercial = No
| location = USA
| type = [[Online encyclopedia]]
| registration = No
| author = Norman Megill
| owner = Norman Megill
}}

मेटामैथ प्रमाण अन्वेषक (एसईटी.एमएम में अभिलेखबद्ध किया गया) मुख्य और अब तक का सबसे बड़ा आंकड़ाकोष है, जिसके जुलाई 2019 तक इसके मुख्य भाग में 23,000 से अधिक प्रमाण हैं। यह शास्त्रीय प्रथम-क्रम तर्क और जेडएफसी सम्मुच्चय सिद्धांत पर आधारित है (साथ में) आवश्यकता पड़ने पर [[टार्स्की-ग्रोथेंडिक सेट थ्योरी|टार्स्की-ग्रोथेंडिक सम्मुच्चय सिद्धांत]] को जोड़ना, उदाहरण के लिए [[श्रेणी सिद्धांत]] में)। आंकड़ाकोष को बीस वर्षों से अधिक समय तक बनाए रखा गया है (सम्मुच्चय.एमएम में पहला प्रमाण अगस्त 1993 का है)। आंकड़ाकोष में अन्य क्षेत्रों के बीच, सम्मुच्चय सिद्धांत (ऑर्डिनल्स और कार्डिनल्स, रिकर्सन, पसंद के स्वयंसिद्ध के समकक्ष, सातत्य परिकल्पना ...), वास्तविक और जटिल संख्या प्रणालियों का निर्माण, अनुक्रम सिद्धांत, आरेख सिद्धांत, के विकास सम्मिलित हैं। सार बीजगणित, रैखिक बीजगणित, सामान्य सांस्थिति, वास्तविक और जटिल विश्लेषण, हिल्बर्ट रिक्त स्थान, संख्या सिद्धांत और प्राथमिक ज्यामिति है। यह आंकड़ाकोष पहले वास्तुशैली मेगिल द्वारा बनाया गया था, लेकिन 2019-10-04 तक इसमें 48 योगदानकर्ता (वास्तुशैली मेगिल सहित) रहे हैं।<ref name="gource">{{cite web | author=Wheeler, David A. | title=Metamath set.mm contributions viewed with Gource through 2019-10-04 | website=[[YouTube]] | url=https://www.youtube.com/watch?v=XC1g8FmFcUU |archive-url=https://ghostarchive.org/varchive/youtube/20211219/XC1g8FmFcUU |archive-date=2021-12-19 |url-status=live}}{{cbignore}}</ref>

मेटामैथ प्रमाण अन्वेषक कई पाठ्य पुस्तकों का संदर्भ देता है जिनका उपयोग मेटामैथ के संयोजन में किया जा सकता है। <ref name="reading">{{cite web | author=Megill, Norman | title=सुझाव पढ़ना| work=Metamath |url=http://us2.metamath.org:8888/mpegif/mmset.html#read}}</ref> इस प्रकार, गणित के अध्ययन में रुचि रखने वाले लोग इन पुस्तकों के संबंध में मेटामैथ का उपयोग कर सकते हैं और यह सत्यापित कर सकते हैं कि सिद्ध कथन साहित्य से मेल खाते हैं।

=== [[अंतर्ज्ञानवादी तर्क]] अन्वेषक ===
यह आंकड़ाकोष एक रचनात्मक दृष्टिकोण से गणित को विकसित करता है, अंतर्ज्ञानवादी तर्क के सिद्धांतों से प्रारम्भ होता है और [[रचनात्मक सेट सिद्धांत|रचनात्मक सम्मुच्चय सिद्धांत]] के स्वयंसिद्ध प्रणालियों के साथ जारी रहता है।

=== [[नई नींव]] अन्वेषक ===
यह आंकड़ाकोष क्वीन्स नवीन आधार सम्मुच्चय सिद्धांत से गणित विकसित करता है।

=== [[उच्च क्रम तर्क]] अन्वेषक ===
यह आंकड़ाकोष उच्च-क्रम तर्क के साथ प्रारम्भ होता है और प्रथम-क्रम तर्क और जेडएफसी सम्मुच्चय सिद्धांत के स्वयंसिद्धों के समकक्ष प्राप्त करता है।

=== खोजकर्ता के बिना आंकड़ाकोष ===
मेटामैथ वेबसाइट कुछ अन्य आंकड़ाकोष को आयोजित करती है जो खोजकर्ताओं से संबद्ध नहीं हैं लेकिन फिर भी उल्लेखनीय हैं। [[रॉबर्ट सोलोवे]] द्वारा लिखित आंकड़ाकोष पीनो.एमएम [[पियानो अंकगणित]] को औपचारिक रूप देता है। आंकड़ाकोष एनएटी.एमएम <ref name="natmm">{{cite web | author=Liné, Frédéric | title=प्राकृतिक कटौती आधारित मेटामैथ प्रणाली| url=http://wiki.planetmath.org/cgi-bin/wiki.pl/Natural_deduction_based_metamath_system | url-status=dead | archiveurl=https://archive.today/20121228041230/http://wiki.planetmath.org/cgi-bin/wiki.pl/Natural_deduction_based_metamath_system | archivedate=2012-12-28 }}</ref> [[प्राकृतिक कटौती]] को औपचारिक रूप देता है। आंकड़ाकोष एमआईयू.एमएम गोडेल, एस्चर, बाच में प्रस्तुत औपचारिक प्रणाली एमआईयू के आधार पर एमयू पहेली को औपचारिक रूप देता है।

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

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

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

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

=== प्रमाण जाँचकर्ता ===
मेटामैथ में लागू किए गए अभिकल्पना विचारों का उपयोग करते हुए, [[राफ लेविन]] ने पायथन कोड की केवल 500 रेखाओं पर बहुत छोटे प्रमाण जाँचकर्ता, एमएमवीईआरआईएफवाई.पीवाई को लागू किया है।

गिल्बर्ट एमएमवीईआरआईएफवाई.पीवाई पर आधारित समान यद्यपि अधिक विस्तृत भाषा है। <ref name="ghilbert">{{cite web | author=Levien,Raph | title=गिल्बर्ट| url=https://ghilbert-app.appspot.com}}</ref> लेविन एक ऐसी प्रणाली को लागू करना चाहते हैं जहां कई लोग सहयोग कर सकें और उनका काम प्रतिरुपकता और छोटे सिद्धांतों के बीच संबंध पर जोर दे रहा है।

लेविएन मौलिक कार्यों का उपयोग करते हुए, मेटामैथ अभिकल्पना सिद्धांतों के कई अन्य कार्यान्वयन विभिन्न प्रकार की भाषाओं के लिए लागू किए गए हैं। जुहा अर्पियेनेन ने [[ सामान्य लिस्प | सामान्य लिस्प]] में बोर्बाकी नामक अपना स्वयं का प्रमाण़ जाँचकर्ता कार्यान्वित किया है <ref name="bourbaki">{{cite web | author=Arpiainen, Juha | title=बोरबाकी की प्रस्तुति| url=http://wiki.planetmath.org/cgi-bin/wiki.pl/Bourbaki_proof_checker | url-status=dead | archiveurl=https://archive.today/20121228115800/http://wiki.planetmath.org/cgi-bin/wiki.pl/Bourbaki_proof_checker | archivedate=2012-12-28 }}</ref> और मार्निक्स कलोस्टर ने हम्म नामक [[ हास्केल (प्रोग्रामिंग भाषा) |हास्केल (प्रोग्रामिंग भाषा)]] में एक प्रमाण जाँचकर्ता को कोडित किया है।<ref name="Hmm">{{cite web | author=Klooster,Marnix | title=हम्म की प्रस्तुति| url=http://wiki.planetmath.org/cgi-bin/wiki.pl/Hmm | url-status=dead | archiveurl=https://web.archive.org/web/20120402081636/http://wiki.planetmath.org/cgi-bin/wiki.pl/Hmm | archivedate=2012-04-02 }}</ref>

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

=== संपादक ===
मेल ओ'कैट ने एमएमजे2 नामक एक सिस्टम अभिकल्पित किया है, जो प्रमाण प्रविष्टि के लिए [[ग्राफिक यूजर इंटरफेस|आरेखिक उपभोक्ता अंतरापृष्ठ]] प्रदान करता है। <ref name="mmj2">{{cite web|author=O'Cat,Mel |title=Presentation of mmj2 |url=http://wiki.planetmath.org/cgi-bin/wiki.pl/mmj2 |url-status=dead |archiveurl=https://web.archive.org/web/20131219001737/http://wiki.planetmath.org/cgi-bin/wiki.pl/mmj2 |archivedate=December 19, 2013 }}</ref> मेल ओ'काट का प्रारंभिक उद्देश्य उपयोगकर्ता को केवल सूत्रों को टाइप करके प्रमाण सम्मिलित करने की अनुमति देना था और एमएमजे2 को उन्हें जोड़ने के लिए उपयुक्त अनुमान नियम खोजने देना था। इसके विपरीत मेटामैथ में आप केवल प्रमेयों के नाम सम्मिलित कर सकते हैं। आप सीधे सूत्र सम्मिलित नहीं कर सकते हैं। एमएमजे2 में प्रमाण को आगे या पीछे प्रवेश करने की भी संभावना है (मेटामथ केवल प्रमाण पश्चगामी में प्रवेश करने की अनुमति देता है)। इसके अतिरिक्त एमएमजे 2 में वास्तविक व्याकरण पार्सर है (मेटामैथ के विपरीत)। यह तकनीकी अंतर उपयोगकर्ता को अधिक सुविधा प्रदान करता है। विशेष रूप से मेटामैथ कभी-कभी कई सूत्रों के बीच झिझकता है जो इसका विश्लेषण करता है (उनमें से अधिकतर व्यर्थ हैं) और उपयोगकर्ता को चुनने के लिए कहता है। एमएमजे2 में यह सीमा अब उपस्थित नहीं है।

मेटामैथ में एममाइड नामक एक आरेखिकल उपभोक्ता अंतरापृष्ठ जोड़ने के लिए विलियम हेल द्वारा एक परियोजना भी है। <ref name="mmide">{{cite web | author=Hale, William | title=एममाइड की प्रस्तुति| url=http://wiki.planetmath.org/cgi-bin/wiki.pl/mmide | url-status=dead | archiveurl=https://archive.today/20121228044320/http://wiki.planetmath.org/cgi-bin/wiki.pl/mmide | archivedate=2012-12-28 }}</ref> पॉल चैपमैन अपनी बारी में एक नए प्रमाण ब्राउज़र पर काम कर रहे हैं, जिसमें हाइलाइटिंग है जो आपको प्रतिस्थापन के पहले और बाद में संदर्भित प्रमेय को देखने की अनुमति देता है।

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

== यह भी देखें ==
* [[स्वचालित सबूत जाँच|स्वचालित प्रमाण जाँच]]
* [[सबूत सहायक|प्रमाण सहायक]]

==संदर्भ==
{{Reflist}}


==बाहरी संबंध==
* [http://us.metamath.org मेटामैथ]: आधिकारिक वेबसाइट.
* [http://www.quora.com/What-do-mathematicians-think-of-Metamath गणितज्ञ मेटामैथ के बारे में क्या सोचते हैं?]: मेटामैथ पर राय.
[[Category: मुफ्त गणित सॉफ्टवेयर]] [[Category: नि: शुल्क प्रमेय समर्थक]] [[Category: बड़े पैमाने पर गणितीय औपचारिकता परियोजनाएं]] [[Category: सबूत सहायक]] 



[[Category: Machine Translated Page]]
[[Category:Created On 02/06/2023]]