मेटामैथ: Difference between revisions

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

Metamath
Developer(s)	Norman Megill
Initial release	0.07 in June 2005; 19 years ago
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.
Written in	ANSI C
Operating system	Linux, Windows, macOS
Type	Computer-assisted proof checking
License	GNU General Public License (Creative Commons Public Domain Dedication for databases)
Website	metamath.org

Revision as of 10:09, 27 June 2023

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

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

मेटामथ भाषा

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

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

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

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

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

$( 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 ) $.

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

<पूर्व> $(राज्य स्वयंसिद्ध 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 $.
    $}

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

प्रमाण

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

  $( 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
     $.

$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 मेटामैथ प्रमाण अन्वेषक (एसईटी.एमएम) में बाईं ओर दर्शाया गया है। आइए बताते हैं कि जब आप प्रमेय का उपयोग करते हैं तो चरण 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 है।

मेटामैथ प्रमाण जाँचकर्ता

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

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

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

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

\vdash \varphi \quad \&\quad \vdash (\varphi \rightarrow \psi )\quad \Rightarrow \quad \vdash \psi

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

मेटामैथ आंकड़ाकोष

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

मेटामैथ प्रमाण अन्वेषक

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

मेटामैथ प्रमाण अन्वेषक कई पाठ्य पुस्तकों का संदर्भ देता है जिनका उपयोग मेटामैथ के संयोजन में किया जा सकता है। ^[10] इस प्रकार, गणित के अध्ययन में रुचि रखने वाले लोग इन पुस्तकों के संबंध में मेटामैथ का उपयोग कर सकते हैं और यह सत्यापित कर सकते हैं कि सिद्ध कथन साहित्य से मेल खाते हैं।

अंतर्ज्ञानवादी तर्क अन्वेषक

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

नई नींव अन्वेषक

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

उच्च क्रम तर्क अन्वेषक

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

खोजकर्ता के बिना आंकड़ाकोष

मेटामैथ वेबसाइट कुछ अन्य आंकड़ाकोष को आयोजित करती है जो खोजकर्ताओं से संबद्ध नहीं हैं लेकिन फिर भी उल्लेखनीय हैं। रॉबर्ट सोलोवे द्वारा लिखित आंकड़ाकोष पीनो.एमएम पियानो अंकगणित को औपचारिक रूप देता है। आंकड़ाकोष एनएटी.एमएम ^[11] प्राकृतिक कटौती को औपचारिक रूप देता है। आंकड़ाकोष एमआईयू.एमएम गोडेल, एस्चर, बाच में प्रस्तुत औपचारिक प्रणाली एमआईयू के आधार पर एमयू पहेली को औपचारिक रूप देता है।

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

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

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

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

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

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

प्रमाण जाँचकर्ता

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

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

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

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

संपादक

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

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

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

यह भी देखें

संदर्भ

↑ 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.
↑ Megill, Norman. "What is Metamath?". Metamath Home Page.
↑ Metamath 100.
↑ "Formalizing 100 Theorems".
↑ Megill, Norman. "ज्ञात मेटामैथ प्रूफ सत्यापनकर्ता". Retrieved 8 October 2022.
↑ TOC of Theorem List - Metamath Proof Explorer
↑ Megill,Norman. "सबूत कैसे काम करते हैं". Metamath Proof Explorer Home Page.
↑ Megill, Norman. "ज्ञात मेटामैथ प्रूफ सत्यापनकर्ता". Retrieved 8 October 2022.
↑ Wheeler, David A. "Metamath set.mm contributions viewed with Gource through 2019-10-04". YouTube. Archived from the original on 2021-12-19.
↑ Megill, Norman. "सुझाव पढ़ना". Metamath.
↑ Liné, Frédéric. "प्राकृतिक कटौती आधारित मेटामैथ प्रणाली". Archived from the original on 2012-12-28.
↑ Levien,Raph. "गिल्बर्ट".
↑ Arpiainen, Juha. "बोरबाकी की प्रस्तुति". Archived from the original on 2012-12-28.
↑ Klooster,Marnix. "हम्म की प्रस्तुति". Archived from the original on 2012-04-02.
↑ O'Cat,Mel. "Presentation of mmj2". Archived from the original on December 19, 2013.
↑ Hale, William. "एममाइड की प्रस्तुति". Archived from the original on 2012-12-28.

बाहरी संबंध

मेटामैथ: आधिकारिक वेबसाइट.
गणितज्ञ मेटामैथ के बारे में क्या सोचते हैं?: मेटामैथ पर राय.

[metamath-book-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

[howpswork-7] Megill,Norman. "सबूत कैसे काम करते हैं". Metamath Proof Explorer Home Page.

[8] Megill, Norman. "ज्ञात मेटामैथ प्रूफ सत्यापनकर्ता". Retrieved 8 October 2022.

[gource-9] Wheeler, David A. "Metamath set.mm contributions viewed with Gource through 2019-10-04". YouTube. Archived from the original on 2021-12-19.

[reading-10] Megill, Norman. "सुझाव पढ़ना". Metamath.

[natmm-11] Liné, Frédéric. "प्राकृतिक कटौती आधारित मेटामैथ प्रणाली". Archived from the original on 2012-12-28.

[ghilbert-12] Levien,Raph. "गिल्बर्ट".

[bourbaki-13] Arpiainen, Juha. "बोरबाकी की प्रस्तुति". Archived from the original on 2012-12-28.

[Hmm-14] Klooster,Marnix. "हम्म की प्रस्तुति". Archived from the original on 2012-04-02.

[mmj2-15] O'Cat,Mel. "Presentation of mmj2". Archived from the original on December 19, 2013.

[mmide-16] Hale, William. "एममाइड की प्रस्तुति". Archived from the original on 2012-12-28.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

Anonymous

Search

मेटामैथ: Difference between revisions

Namespaces

More

Page actions

Revision as of 10:09, 27 June 2023

Contents

मेटामथ भाषा

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

प्रमाण

प्रतिस्थापन

मेटामैथ प्रमाण जाँचकर्ता

मेटामैथ आंकड़ाकोष

मेटामैथ प्रमाण अन्वेषक

अंतर्ज्ञानवादी तर्क अन्वेषक

नई नींव अन्वेषक

उच्च क्रम तर्क अन्वेषक

खोजकर्ता के बिना आंकड़ाकोष

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

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

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

प्रमाण जाँचकर्ता

संपादक

यह भी देखें

संदर्भ

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

@@ Line 1: / Line 1: @@
 {{Short description|Formal language and associated computer program}}
-{{For|the study of mathematics using mathematical methods|Metamathematics}}
+{{For|गणितीय विधियों का उपयोग करके गणित का अध्ययन|मेटामैथमैटिक्स}}
 {{Infobox software
 |name = Metamath
@@ Line 15: / Line 15: @@
 }}
-मेटामैथ एक [[औपचारिक भाषा]] है और गणितीय प्रमाणों का संग्रह, सत्यापन और अध्ययन करने के लिए एक संबद्ध कंप्यूटर प्रोग्राम (एक [[ सबूत चेकर ]]) है।<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>
+'''मेटामैथ''' एक [[औपचारिक भाषा]] है और गणितीय प्रमाणों का संग्रह, सत्यापन और अध्ययन करने के लिए एक संबद्ध कंप्यूटर प्रोग्राम (एक [[ सबूत चेकर | प्रमाण जाँचकर्ता]] ) है। <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}}, मेटामैथ का उपयोग करके सिद्ध प्रमेय का सेट औपचारिक गणित के सबसे बड़े निकायों में से एक है, जिसमें 74 के विशेष प्रमाण शामिल हैं<ref>[http://us.metamath.org/mm_100.html Metamath 100.]</ref> औपचारिक 100 प्रमेय चुनौती के 100 प्रमेयों में से,<ref>{{cite web | url=https://www.cs.ru.nl/~freek/100/ | title=Formalizing 100 Theorems }}</ref> [[एचओएल लाइट]], [[ इसाबेल (सबूत सहायक) ]] और [[कोक]] के बाद चौथे स्थान पर रही, लेकिन [[ मिज़ार प्रणाली ]], [[ प्रूफ पावर ]], [[ लीन (सबूत सहायक) ]], एनकथम, [[ACL2]] और एनयूपीआरएल से पहले। मेटामैथ प्रारूप का उपयोग करने वाले डेटाबेस के लिए कम से कम 19 प्रमाण सत्यापनकर्ता हैं।<ref>{{cite web |last1=Megill |first1=Norman |title=ज्ञात मेटामैथ प्रूफ सत्यापनकर्ता|url=http://us.metamath.org/other.html#verifiers |accessdate=8 October 2022}}</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>
-यह परियोजना अपनी तरह की पहली परियोजना है जो एक साधारण वेबसाइट के रूप में अपने औपचारिक प्रमेय डेटाबेस के इंटरैक्टिव ब्राउज़िंग की अनुमति देती है।<ref>[http://us2.metamath.org:88/mpeuni/mmtheorems.html TOC of Theorem List - Metamath Proof Explorer]</ref>
 == मेटामथ भाषा ==
-मेटामैथ भाषा एक धातुभाषा है, जो विभिन्न प्रकार की औपचारिक प्रणालियों के विकास के लिए उपयुक्त है। मेटामैथ भाषा में कोई विशिष्ट तर्क सन्निहित नहीं है। इसके बजाय, इसे केवल यह साबित करने के तरीके के रूप में माना जा सकता है कि अनुमान नियम (स्वयंसिद्ध या बाद में सिद्ध किए गए) को लागू किया जा सकता है।
+मेटामैथ भाषा एक धातुभाषा है, जो विभिन्न प्रकार की औपचारिक प्रणालियों के विकास के लिए उपयुक्त है। मेटामैथ भाषा में कोई विशिष्ट तर्क सन्निहित नहीं है। इसके स्थान पर, इसे केवल यह सिद्ध करने के तरीके के रूप में माना जा सकता है कि अनुमान नियम (स्वयंसिद्ध या बाद में सिद्ध किए गए) को लागू किया जा सकता है।
-प्रमाणित प्रमेयों का सबसे बड़ा डेटाबेस पारंपरिक [[ZFC]] सेट सिद्धांत और क्लासिक लॉजिक का अनुसरण करता है, लेकिन अन्य डेटाबेस मौजूद हैं और अन्य बनाए जा सकते हैं।
+प्रमाणित प्रमेयों का सबसे बड़ा आंकड़ाकोष पारंपरिक [[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>
-मेटामैथ भाषा डिजाइन सादगी पर केंद्रित है; परिभाषाओं, स्वयंसिद्धों, अनुमान नियमों और प्रमेयों को बताने के लिए नियोजित भाषा केवल कुछ मुट्ठी भर खोजशब्दों से बनी होती है, और चर के प्रतिस्थापन के आधार पर एक सरल एल्गोरिथ्म का उपयोग करके सभी प्रमाणों की जाँच की जाती है (वैकल्पिक प्रावधानों के साथ कि किस चर को अलग रहना चाहिए) प्रतिस्थापन के बाद)।<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> (चर प्रतीक) कथन; उदाहरण के लिए:
+सूत्रों के निर्माण के लिए उपयोग किए जा सकने वाले प्रतीकों का सम्मुच्चय <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 (स्वयंसिद्ध अभिकथन) कथनों के संयोजन का उपयोग करके निर्दिष्ट किया गया है; उदाहरण के लिए:
-    $c 0 + = -> ( ) शब्द wff |- $.
+     $( Specify properties of the metavariables $)
-$( उन मेटावेरिएबल्स की घोषणा करें जिनका हम $ उपयोग करेंगे)
-     $v t r s P Q $।
-</पूर्व>
-सूत्रों के लिए व्याकरण के संयोजन का उपयोग करके निर्दिष्ट किया गया है <code>$f</code> (फ्लोटिंग (वैरिएबल-टाइप)
+     tt $f term t $.
-परिकल्पना) और <code>$a</code> (स्वयंसिद्ध अभिकथन) कथन; उदाहरण के लिए:
+     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 ) $.
-<पूर्व>
-$( मेटावेरिएबल्स के गुण निर्दिष्ट करें $)
-    टीटी $ च अवधि टी $।
-    tr $f अवधि r $।
-    टीएस $ च अवधि एस $।
-    डब्ल्यूपी $एफ डब्ल्यूएफएफ पी $।
-    wq $f wff क्यू $।
-$(wff परिभाषित करें (भाग 1) $)
-    Weq $a wff t = r $.
-$(wff परिभाषित करें (भाग 2) $)
-    wim $a wff ( P -> Q ) $.
-</पूर्व>
-अभिगृहीतों और अनुमान के नियमों को निर्दिष्ट किया गया है <code>$a</code> साथ में बयान <code>${</code> और <code>$}</code> ब्लॉक स्कूपिंग और वैकल्पिक के लिए <code>$e</code> (आवश्यक परिकल्पना) कथन; उदाहरण के लिए:
+अभिगृहीतों और अनुमान के नियमों को निर्दिष्ट किया गया है <code>$a</code> साथ में बयान <code>${</code> और <code>$}</code> खण्ड परिदृश्यन और वैकल्पिक <code>$e</code> (आवश्यक परिकल्पना) कथन के लिए है; उदाहरण के लिए:
 <पूर्व>
 $(राज्य स्वयंसिद्ध a1 $)
-    a1 $a |- (t = r -> (t = s -> r = s)) $।
+   $( State axiom a1 $)
-$(राज्य स्वयंसिद्ध a2 $)
-    a2 $a |- (t + 0) = t $।
-    ${
-       मिन $ई |-पी $।
-       माज $ई |- (पी -> क्यू) $।
-$(मॉडस पोनेन्स इंट्रेंस रूल को परिभाषित करें $)
-       एमपी $ ए |- क्यू $।
-    $}
-</पूर्व>
-एक निर्माण का उपयोग करना, <code>$a</code> कथन, सिंटैक्टिक नियमों, स्वयंसिद्ध स्कीमाओं और अनुमान के नियमों को पकड़ने के लिए एक जटिल प्रकार की प्रणाली पर निर्भरता के बिना LF (तार्किक ढांचे) के समान लचीलेपन का स्तर प्रदान करने का इरादा है।
+     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: $)
-    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 weq tt tt weq tt a2 tt tze tpl
+        tt tze tpl tt tt a1 mp mp
-       tt weq tt tze tpl tt weq tt tt weq wim tt a2
+      $.
-       tt tze tpl tt tt a1 mp mp
+<code>$p</code> कथन में प्रमाण को सम्मिलित करने पर ध्यान दें। यह निम्नलिखित विस्तृत प्रमाण को संक्षिप्त करता है:
-     $।
-</पूर्व>
-में प्रमाण को शामिल करने पर ध्यान दें <code>$p</code> कथन। यह निम्नलिखित विस्तृत प्रमाण को संक्षिप्त करता है:
 <syntaxhighlight line lang="nasm">
@@ Line 105: / Line 100: @@
 ,5,6,16 mp   $a |- t = t
 </syntaxhighlight>
-सबूत का आवश्यक रूप एक अधिक परंपरागत प्रस्तुति छोड़कर, वाक्यात्मक विवरण को समाप्त करता है:
+प्रमाण का आवश्यक रूप एक अधिक परंपरागत प्रस्तुति छोड़कर, वाक्यात्मक विवरण को समाप्त करता है:
 <syntaxhighlight line lang="nasm">
@@ Line 117: / Line 112: @@
 === प्रतिस्थापन ===
-[[Image:Proofstep.gif|thumb|right|592px|चरण-दर-चरण प्रमाण]]सभी मेटामैथ प्रूफ स्टेप्स एक एकल प्रतिस्थापन नियम का उपयोग करते हैं, जो एक अभिव्यक्ति के साथ एक चर का सरल प्रतिस्थापन है और विधेय कलन पर काम में वर्णित उचित प्रतिस्थापन नहीं है। मेटामैथ डेटाबेस में इसका समर्थन करने वाले उचित प्रतिस्थापन, मेटामैथ भाषा में निर्मित एक के बजाय एक व्युत्पन्न निर्माण है।
+[[Image:Proofstep.gif|thumb|right|592px|चरण-दर-चरण प्रमाण]]सभी मेटामैथ प्रमाण चरण एक एकल प्रतिस्थापन नियम का उपयोग करते हैं, जो एक अभिव्यक्ति के साथ एक चर का सरल प्रतिस्थापन है और विधेय कलन पर काम में वर्णित उचित प्रतिस्थापन नहीं है। मेटामैथ आंकड़ाकोष में इसका समर्थन करने वाले उचित प्रतिस्थापन, मेटामैथ भाषा में निर्मित एक के स्थान पर एक व्युत्पन्न निर्माण है।
 प्रतिस्थापन नियम उपयोग में तर्क प्रणाली के बारे में कोई धारणा नहीं बनाता है और केवल यह आवश्यक है कि चर के प्रतिस्थापन सही तरीके से किए जाएं।
-यह एल्गोरिदम कैसे काम करता है इसका एक विस्तृत उदाहरण यहां दिया गया है। प्रमेय के चरण 1 और 2 <code>2p2e4</code> मेटामैथ प्रूफ एक्सप्लोरर (set.mm) में बाईं ओर दर्शाया गया है। आइए बताते हैं कि जब आप प्रमेय का उपयोग करते हैं तो चरण 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>. यहाँ एकीकरण केवल स्थिरांक का मामला है और सीधा है (स्थानापन्न करने के लिए चर की कोई समस्या नहीं है)। तो सत्यापन समाप्त हो गया है और प्रमाण के ये दो चरण हैं <code>2p2e4</code> सही हैं।
+यह कलन विधि कैसे काम करता है इसका एक विस्तृत उदाहरण यहां दिया गया है। प्रमेय के चरण 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> है।
-जब मेटामैथ एकीकृत होता है {{math|1=( 2 + 2 )}} साथ {{magenta|{{mvar|B}}}} यह जांचना है कि वाक्य-विन्यास के नियमों का सम्मान किया जाता है। वास्तव में {{magenta|{{mvar|B}}}} का प्रकार है <code>class</code> इस प्रकार मेटामैथ को इसकी जांच करनी है {{math|1=( 2 + 2 )}} भी टाइप किया गया है <code>class</code>.
+== मेटामैथ प्रमाण जाँचकर्ता ==
+मेटामैथ प्रोग्राम मेटामैथ भाषा का उपयोग करके लिखे गए आंकड़ाकोष में हस्त कौशल करने के लिए बनाया गया मूल प्रोग्राम है। इसमें एक पाठ (कमांड लाइन) अंतरापृष्ठ है और इसे C में लिखा गया है। यह मेटामैथ आंकड़ाकोष को मेमोरी में पढ़ सकता है, आंकड़ाकोष के प्रमाण को सत्यापित कर सकता है, आंकड़ाकोष को संशोधित कर सकता है (विशेष रूप से प्रमाण जोड़कर), और उन्हें स्टोरेज में वापस लिख सकता है।
-== मेटामैथ प्रूफ चेकर ==
+इसमें एक सिद्ध कमांड है जो उपयोगकर्ताओं को उपस्थिता प्रमाणों की खोज के लिए तंत्र के साथ-साथ एक प्रमाण सम्मिलित करने में सक्षम बनाता है।
-मेटामैथ प्रोग्राम मेटामैथ भाषा का उपयोग करके लिखे गए डेटाबेस में हेरफेर करने के लिए बनाया गया मूल प्रोग्राम है। इसमें एक [[टेक्स]]्ट (कमांड लाइन) इंटरफेस है और इसे सी में लिखा गया है। यह मेटामैथ डेटाबेस को मेमोरी में पढ़ सकता है, डेटाबेस के प्रूफ को सत्यापित कर सकता है, डेटाबेस को संशोधित कर सकता है (विशेष रूप से प्रूफ जोड़कर), और उन्हें स्टोरेज में वापस लिख सकता है।
-इसमें एक सिद्ध कमांड है जो उपयोगकर्ताओं को मौजूदा प्रमाणों की खोज के लिए तंत्र के साथ-साथ एक प्रमाण दर्ज करने में सक्षम बनाता है।
+मेटामैथ प्रोग्राम वर्णन को [[HTML|एचटीएमएल]] या टीईएक्स संकेत पद्धति में बदल सकता है;
-मेटामैथ प्रोग्राम स्टेटमेंट को [[HTML]] या TeX नोटेशन में बदल सकता है;
+उदाहरण के लिए, यह एसईटी.एमएम से [[modus ponens|विधानात्मक हेतुफलानुमान]] सूक्ति को प्रक्षेपण कर सकता है:
-उदाहरण के लिए, यह set.mm से [[modus ponens]] axiom को आउटपुट कर सकता है:
 :<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>
+कई अन्य प्रोग्राम मेटामैथ आंकड़ाकोष को संसाधित कर सकते हैं, विशेष रूप से, मेटामैथ प्रारूप का उपयोग करने वाले आंकड़ाकोष के लिए कम से कम 19 प्रमाण सत्यापनकर्ता हैं। <ref>{{cite web |last1=Megill |first1=Norman |title=ज्ञात मेटामैथ प्रूफ सत्यापनकर्ता|url=http://us.metamath.org/other.html#verifiers |accessdate=8 October 2022}}</ref>
-== मेटामैथ डेटाबेस ==
+== मेटामैथ आंकड़ाकोष ==
-मेटामैथ वेबसाइट कई डेटाबेस होस्ट करती है जो विभिन्न स्वयंसिद्ध प्रणालियों से प्राप्त प्रमेयों को संग्रहीत करती है। अधिकांश डेटाबेस (.mm फ़ाइलें) में एक संबद्ध इंटरफ़ेस होता है, जिसे एक्सप्लोरर कहा जाता है, जो उपयोगकर्ता के अनुकूल तरीके से वेबसाइट पर बयानों और सबूतों को अंतःक्रियात्मक रूप से नेविगेट करने की अनुमति देता है। अधिकांश डेटाबेस औपचारिक कटौती की [[हिल्बर्ट प्रणाली]] का उपयोग करते हैं, हालांकि यह एक आवश्यकता नहीं है।
+मेटामैथ वेबसाइट कई आंकड़ाकोष आयोजित करती है जो विभिन्न स्वयंसिद्ध प्रणालियों से प्राप्त प्रमेयों को संग्रहीत करती है। अधिकांश आंकड़ाकोष (.mm फ़ाइलें) में एक संबद्ध अंतरापृष्ठ होता है, जिसे अन्वेषक कहा जाता है, जो उपयोगकर्ता के अनुकूल तरीके से वेबसाइट पर बयानों और प्रमाणों को अंतःक्रियात्मक रूप से मार्गनिर्देशन करने की अनुमति देता है। अधिकांश आंकड़ाकोष औपचारिक कटौती की [[हिल्बर्ट प्रणाली]] का उपयोग करते हैं, हालांकि यह एक आवश्यकता नहीं है।
-=== मेटामैथ प्रूफ एक्सप्लोरर ===
+=== मेटामैथ प्रमाण अन्वेषक ===
 {{Infobox website
 | name = Metamath Proof Explorer
@@ Line 154: / Line 151: @@
 }}
-मेटामैथ प्रूफ एक्सप्लोरर (set.mm में रिकॉर्ड किया गया) मुख्य और अब तक का सबसे बड़ा डेटाबेस है, जिसके जुलाई 2019 तक इसके मुख्य भाग में 23,000 से अधिक प्रूफ हैं। यह शास्त्रीय प्रथम-क्रम तर्क और ZFC सेट सिद्धांत पर आधारित है (साथ में) जरूरत पड़ने पर [[टार्स्की-ग्रोथेंडिक सेट थ्योरी]] को जोड़ना, उदाहरण के लिए [[श्रेणी सिद्धांत]] में)। डेटाबेस को बीस वर्षों से अधिक समय तक बनाए रखा गया है (सेट.एमएम में पहला प्रमाण अगस्त 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>
+मेटामैथ प्रमाण अन्वेषक (एसईटी.एमएम में अभिलेखबद्ध किया गया) मुख्य और अब तक का सबसे बड़ा आंकड़ाकोष है, जिसके जुलाई 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="reading">{{cite web | author=Megill, Norman | title=सुझाव पढ़ना| work=Metamath |url=http://us2.metamath.org:8888/mpegif/mmset.html#read}}</ref> इस प्रकार, गणित के अध्ययन में रुचि रखने वाले लोग इन पुस्तकों के संबंध में मेटामैथ का उपयोग कर सकते हैं और यह सत्यापित कर सकते हैं कि सिद्ध कथन साहित्य से मेल खाते हैं।
-यह डेटाबेस एक रचनात्मक दृष्टिकोण से गणित को विकसित करता है, अंतर्ज्ञानवादी तर्क के सिद्धांतों से शुरू होता है और [[रचनात्मक सेट सिद्धांत]] के स्वयंसिद्ध प्रणालियों के साथ जारी रहता है।
-=== [[नई नींव]] एक्सप्लोरर ===
+=== [[अंतर्ज्ञानवादी तर्क]] अन्वेषक ===
-यह डेटाबेस Quine's New Foundations set Theory से गणित विकसित करता है।
+यह आंकड़ाकोष एक रचनात्मक दृष्टिकोण से गणित को विकसित करता है, अंतर्ज्ञानवादी तर्क के सिद्धांतों से प्रारम्भ होता है और [[रचनात्मक सेट सिद्धांत|रचनात्मक सम्मुच्चय सिद्धांत]] के स्वयंसिद्ध प्रणालियों के साथ जारी रहता है।
-=== [[उच्च क्रम तर्क]] एक्सप्लोरर ===
+=== [[नई नींव]] अन्वेषक ===
-यह डेटाबेस उच्च-क्रम तर्क के साथ शुरू होता है और प्रथम-क्रम तर्क और ZFC सेट सिद्धांत के स्वयंसिद्धों के समकक्ष प्राप्त करता है।
+यह आंकड़ाकोष क्वीन्स नवीन आधार सम्मुच्चय सिद्धांत से गणित विकसित करता है।
-=== खोजकर्ता के बिना डेटाबेस ===
+=== [[उच्च क्रम तर्क]] अन्वेषक ===
-मेटामैथ वेबसाइट कुछ अन्य डेटाबेस को होस्ट करती है जो खोजकर्ताओं से संबद्ध नहीं हैं लेकिन फिर भी उल्लेखनीय हैं। [[रॉबर्ट सोलोवे]] द्वारा लिखित डेटाबेस पीनो.एमएम [[पियानो अंकगणित]] को औपचारिक रूप देता है। डेटाबेस nat.mm<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> [[प्राकृतिक कटौती]] को औपचारिक रूप देता है। डेटाबेस miu.mm Gödel, Escher, Bach में प्रस्तुत औपचारिक प्रणाली MIU के आधार पर MU पहेली को औपचारिक रूप देता है।
+यह आंकड़ाकोष उच्च-क्रम तर्क के साथ प्रारम्भ होता है और प्रथम-क्रम तर्क और जेडएफसी सम्मुच्चय सिद्धांत के स्वयंसिद्धों के समकक्ष प्राप्त करता है।
+=== खोजकर्ता के बिना आंकड़ाकोष ===
+मेटामैथ वेबसाइट कुछ अन्य आंकड़ाकोष को आयोजित करती है जो खोजकर्ताओं से संबद्ध नहीं हैं लेकिन फिर भी उल्लेखनीय हैं। [[रॉबर्ट सोलोवे]] द्वारा लिखित आंकड़ाकोष पीनो.एमएम [[पियानो अंकगणित]] को औपचारिक रूप देता है। आंकड़ाकोष एनएटी.एमएम <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> [[प्राकृतिक कटौती]] को औपचारिक रूप देता है। आंकड़ाकोष एमआईयू.एमएम गोडेल, एस्चर, बाच में प्रस्तुत औपचारिक प्रणाली एमआईयू के आधार पर एमयू पहेली को औपचारिक रूप देता है।
 === पुराने खोजकर्ता ===
-मेटामैथ वेबसाइट कुछ पुराने डेटाबेस को भी होस्ट करती है जो अब बनाए नहीं रखे जाते हैं, जैसे कि हिल्बर्ट स्पेस एक्सप्लोरर, जो [[हिल्बर्ट अंतरिक्ष]] सिद्धांत से संबंधित प्रमेय प्रस्तुत करता है जिसे अब मेटामैथ प्रूफ एक्सप्लोरर में विलय कर दिया गया है, और [[ क्वांटम तर्क ]] एक्सप्लोरर, जो क्वांटम विकसित करता है ऑर्थोमॉड्यूलर लैटिस के सिद्धांत से शुरू होने वाला तर्क।
+मेटामैथ वेबसाइट कुछ पुराने आंकड़ाकोष को भी आयोजित करती है जो अब बनाए नहीं रखे जाते हैं, जैसे कि हिल्बर्ट स्थल अन्वेषक, जो [[हिल्बर्ट अंतरिक्ष]] सिद्धांत से संबंधित प्रमेय प्रस्तुत करता है जिसे अब मेटामैथ प्रमाण अन्वेषक में विलय कर दिया गया है, और [[ क्वांटम तर्क |परिमाण तर्क]] अन्वेषक, जो परिमाण ऑर्थोमॉड्यूलर जालक के सिद्धांत से प्रारम्भ होने वाला तर्क विकसित करता है।
 == प्राकृतिक कटौती ==
-क्योंकि मेटामैथ की एक बहुत ही सामान्य अवधारणा है कि एक प्रमाण क्या है (अर्थात् अनुमान नियमों से जुड़े सूत्रों का एक पेड़) और सॉफ़्टवेयर में कोई विशिष्ट तर्क एम्बेड नहीं किया गया है, मेटामैथ का उपयोग तर्क की प्रजातियों के साथ किया जा सकता है जो हिल्बर्ट-शैली के तर्क या अनुक्रमों के रूप में भिन्न हैं। आधारित लॉजिक्स या [[लैम्ब्डा कैलकुलस]] के साथ भी।
+क्योंकि मेटामैथ की एक बहुत ही सामान्य अवधारणा है कि एक प्रमाण क्या है (अर्थात् अनुमान नियमों से जुड़े सूत्रों का एक तरू) और सॉफ़्टवेयर में कोई विशिष्ट तर्क अंतःस्थापित नहीं किया गया है, मेटामैथ का उपयोग तर्क की प्रजातियों के साथ किया जा सकता है जो हिल्बर्ट-शैली के तर्क या अनुक्रमों के रूप में भिन्न हैं। आधारित तर्क या [[लैम्ब्डा कैलकुलस|लैम्ब्डा कलन]] के साथ भी भिन्न हैं।
+हालाँकि, मेटामैथ प्राकृतिक कटौती प्रणाली के लिए कोई प्रत्यक्ष समर्थन प्रदान नहीं करता है। जैसा कि पहले उल्लेख किया गया है, आंकड़ाकोष एनएटी.एमएमप्राकृतिक कटौती को औपचारिक रूप देता है। मेटामैथ प्रमाण अन्वेषक (इसके आंकड़ाकोष सम्मुच्चय.एमएम के साथ) इसके स्थान पर सम्मेलनों के एक सम्मुच्चय का उपयोग करता है जो हिल्बर्ट-शैली के तर्क के भीतर प्राकृतिक कटौती दृष्टिकोणों के उपयोग की अनुमति देता है।
-हालाँकि, मेटामैथ प्राकृतिक कटौती प्रणाली के लिए कोई प्रत्यक्ष समर्थन प्रदान नहीं करता है। जैसा कि पहले उल्लेख किया गया है, डेटाबेस nat.mm प्राकृतिक कटौती को औपचारिक रूप देता है। मेटामैथ प्रूफ एक्सप्लोरर (इसके डेटाबेस सेट.एमएम के साथ) इसके बजाय सम्मेलनों के एक सेट का उपयोग करता है जो हिल्बर्ट-शैली के तर्क के भीतर प्राकृतिक कटौती दृष्टिकोणों के उपयोग की अनुमति देता है।
+=== मेटामैथ से जुड़े अन्य कार्य ===
-==मेटामैथ== से जुड़े अन्य कार्य
+=== प्रमाण जाँचकर्ता ===
+मेटामैथ में लागू किए गए अभिकल्पना विचारों का उपयोग करते हुए, [[राफ लेविन]] ने पायथन कोड की केवल 500 रेखाओं पर बहुत छोटे प्रमाण जाँचकर्ता, एमएमवीईआरआईएफवाई.पीवाई को लागू किया है।
-=== प्रूफ चेकर्स ===
+गिल्बर्ट एमएमवीईआरआईएफवाई.पीवाई पर आधारित समान यद्यपि अधिक विस्तृत भाषा है। <ref name="ghilbert">{{cite web | author=Levien,Raph | title=गिल्बर्ट| url=https://ghilbert-app.appspot.com}}</ref> लेविन एक ऐसी प्रणाली को लागू करना चाहते हैं जहां कई लोग सहयोग कर सकें और उनका काम प्रतिरुपकता और छोटे सिद्धांतों के बीच संबंध पर जोर दे रहा है।
-मेटामैथ में लागू किए गए डिजाइन विचारों का उपयोग करते हुए, [[राफ लेविन]] ने पायथन कोड की केवल 500 लाइनों पर बहुत छोटे प्रूफ चेकर, mmverify.py को लागू किया है।
-Ghilbert mmverify.py पर आधारित समान यद्यपि अधिक विस्तृत भाषा है।<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>
-लेविएन मौलिक कार्यों का उपयोग करते हुए, मेटामैथ डिजाइन सिद्धांतों के कई अन्य कार्यान्वयन विभिन्न प्रकार की भाषाओं के लिए लागू किए गए हैं। Juha Arpiainen ने [[ सामान्य लिस्प ]] में Bourbaki नामक अपना स्वयं का प्रूफ़ चेकर कार्यान्वित किया है<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> और Marnix Klooster ने Hmm नामक [[ हास्केल (प्रोग्रामिंग भाषा) ]] में एक प्रूफ चेकर को कोडित किया है।<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>
+हालांकि वे सभी औपचारिक सिस्टम जाँचकर्ता कोडिंग के लिए समग्र मेटामैथ दृष्टिकोण का उपयोग करते हैं, वे स्वयं की नई अवधारणाओं को भी लागू करते हैं।
-हालांकि वे सभी औपचारिक सिस्टम चेकर कोडिंग के लिए समग्र मेटामैथ दृष्टिकोण का उपयोग करते हैं, वे स्वयं की नई अवधारणाओं को भी लागू करते हैं।
 === संपादक ===
-Mel O'Cat ने Mmj2 नामक एक सिस्टम डिज़ाइन किया है, जो प्रूफ एंट्री के लिए [[ग्राफिक यूजर इंटरफेस]] प्रदान करता है।<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> मेल ओ'काट का प्रारंभिक उद्देश्य उपयोगकर्ता को केवल सूत्रों को टाइप करके सबूत दर्ज करने की अनुमति देना था और Mmj2 को उन्हें जोड़ने के लिए उपयुक्त अनुमान नियम खोजने देना था। इसके विपरीत मेटामैथ में आप केवल प्रमेयों के नाम दर्ज कर सकते हैं। आप सीधे सूत्र दर्ज नहीं कर सकते हैं। Mmj2 में प्रूफ को आगे या पीछे प्रवेश करने की भी संभावना है (मेटामथ केवल प्रूफ बैकवर्ड में प्रवेश करने की अनुमति देता है)। इसके अलावा एमएमजे 2 में वास्तविक व्याकरण पार्सर है (मेटामैथ के विपरीत)। यह तकनीकी अंतर उपयोगकर्ता को अधिक सुविधा प्रदान करता है। विशेष रूप से मेटामैथ कभी-कभी कई सूत्रों के बीच झिझकता है जो इसका विश्लेषण करता है (उनमें से अधिकतर व्यर्थ हैं) और उपयोगकर्ता को चुनने के लिए कहता है। Mmj2 में यह सीमा अब मौजूद नहीं है।
+मेल ओ'कैट ने एमएमजे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> पॉल चैपमैन अपनी बारी में एक नए प्रूफ ब्राउज़र पर काम कर रहे हैं, जिसमें हाइलाइटिंग है जो आपको प्रतिस्थापन के पहले और बाद में संदर्भित प्रमेय को देखने की अनुमति देता है।
+मेटामैथ में एममाइड नामक एक आरेखिकल उपभोक्ता अंतरापृष्ठ जोड़ने के लिए विलियम हेल द्वारा एक परियोजना भी है। <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> पॉल चैपमैन अपनी बारी में एक नए प्रमाण ब्राउज़र पर काम कर रहे हैं, जिसमें हाइलाइटिंग है जो आपको प्रतिस्थापन के पहले और बाद में संदर्भित प्रमेय को देखने की अनुमति देता है।
-मिलपगेम एक प्रूफ असिस्टेंट और एक चेकर है (यह एक संदेश दिखाता है कि कुछ गलत हो गया है) मेटामैथ लैंग्वेज (सेट.एमएम) के लिए एक ग्राफिक यूजर इंटरफेस के साथ, फिलिप सेर्नाटेस्कू द्वारा लिखा गया है, यह एक ओपन सोर्स (एमआईटी लाइसेंस) जावा एप्लिकेशन है ( क्रॉस-प्लेटफ़ॉर्म एप्लिकेशन: विंडो, लिनक्स, मैक ओएस)। उपयोगकर्ता दो तरीकों से प्रदर्शन (प्रमाण) में प्रवेश कर सकता है: साबित करने के लिए कथन के सापेक्ष आगे और पीछे। Milpgame जाँचता है कि क्या कोई कथन अच्छी तरह से बना है (एक वाक्यात्मक सत्यापनकर्ता है)। यह डमीलिंक प्रमेय के उपयोग के बिना अधूरे प्रमाणों को सहेज सकता है। प्रदर्शन को पेड़ के रूप में दिखाया गया है, बयानों को html परिभाषाओं (टाइपसेटिंग अध्याय में परिभाषित) का उपयोग करके दिखाया गया है। Milpgame को Java .jar (JRE संस्करण 6 अपडेट 24 NetBeans IDE में लिखा गया है) के रूप में वितरित किया गया है।
+मिलपगेम एक प्रमाण सहायक और एक जाँचकर्ता है (यह एक संदेश दिखाता है कि कुछ गलत हो गया है) मेटामैथ भाषा (सम्मुच्चय.एमएम) के लिए एक आरेखिक उपभोक्ता अंतरापृष्ठ के साथ, फिलिप सेर्नाटेस्कू द्वारा लिखा गया है, यह एक ओपन सोर्स (एमआईटी लाइसेंस) जावा एप्लिकेशन है ( क्रॉस-प्लेटफ़ॉर्म एप्लिकेशन: विंडो, लिनक्स, मैक ओएस)। उपयोगकर्ता दो तरीकों से प्रदर्शन (प्रमाण) में प्रवेश कर सकता है: सिद्ध करने के लिए कथन के सापेक्ष आगे और पीछे। मिल्पगेम जाँचता है कि क्या कोई कथन अच्छी तरह से बना है (एक वाक्यात्मक सत्यापनकर्ता है)। यह डमीलिंक प्रमेय के उपयोग के बिना अधूरे प्रमाणों को सहेज सकता है। प्रदर्शन को पेड़ के रूप में दिखाया गया है, बयानों को एचटीएमएल परिभाषाओं (टाइपसम्मुच्चय अध्याय में परिभाषित) का उपयोग करके दिखाया गया है। मिल्पगेम को जावा.जार (जेआरई संस्करण 6 अपडेट 24 नेटबीन्स आईडीई में लिखा गया है) के रूप में वितरित किया गया है।
 == यह भी देखें ==
-* [[स्वचालित सबूत जाँच]]
+* [[स्वचालित सबूत जाँच|स्वचालित प्रमाण जाँच]]
-* [[सबूत सहायक]]
+* [[सबूत सहायक|प्रमाण सहायक]]
 ==संदर्भ==
@@ Line 203: / Line 202: @@
 ==बाहरी संबंध==
-* [http://us.metamath.org Metamath]: official website.
+* [http://us.metamath.org मेटामैथ]: आधिकारिक वेबसाइट.
-* [http://www.quora.com/What-do-mathematicians-think-of-Metamath What do mathematicians think of Metamath]: opinions on Metamath.
+* [http://www.quora.com/What-do-mathematicians-think-of-Metamath गणितज्ञ मेटामैथ के बारे में क्या सोचते हैं?]: मेटामैथ पर राय.
 [[Category: मुफ्त गणित सॉफ्टवेयर]] [[Category: नि: शुल्क प्रमेय समर्थक]] [[Category: बड़े पैमाने पर गणितीय औपचारिकता परियोजनाएं]] [[Category: सबूत सहायक]]

Anonymous

Search

मेटामैथ: Difference between revisions

Revision as of 10:09, 27 June 2023

मेटामथ भाषा

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

प्रमाण

प्रतिस्थापन

मेटामैथ प्रमाण जाँचकर्ता

मेटामैथ आंकड़ाकोष

मेटामैथ प्रमाण अन्वेषक

अंतर्ज्ञानवादी तर्क अन्वेषक

नई नींव अन्वेषक

उच्च क्रम तर्क अन्वेषक

खोजकर्ता के बिना आंकड़ाकोष

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

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

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

प्रमाण जाँचकर्ता

संपादक

यह भी देखें

संदर्भ

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories