प्रमाण सहायक: Difference between revisions
No edit summary |
m (Abhishekkshukla moved page सबूत सहायक to प्रमाण सहायक without leaving a redirect) |
||
(4 intermediate revisions by 4 users not shown) | |||
Line 1: | Line 1: | ||
{{Short description|Software tool to assist with the development of formal proofs by human-machine collaboration}} | {{Short description|Software tool to assist with the development of formal proofs by human-machine collaboration}} | ||
{{for| | {{for|कंप्यूटर विज्ञान में सत्यापन|औपचारिक सत्यापन}} | ||
{{for| | {{for|शैक्षणिक सम्मेलन|इंटरएक्टिव प्रमेय साबित करना (सम्मेलन)}} | ||
{{distinguish| | {{distinguish|इंटरएक्टिव प्रूफ सिस्टम}}[[Image:CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png|thumb|सीओक्यूआईडीई में इंटरएक्टिव प्रूफ सत्र, बाईं ओर प्रूफ स्क्रिप्ट और दाईं ओर प्रूफ स्टेट दिखा रहा है।]][[कंप्यूटर]] विज्ञान और [[गणितीय तर्क]] में, '''प्रमाण सहायक''' या इंटरैक्टिव प्रमेय प्रोवर मानव-मशीन सहयोग से औपचारिक प्रमाण के विकास में सहायता के लिए सॉफ्टवेयर उपकरण है। इसमें कुछ प्रकार के इंटरएक्टिव प्रूफ एडिटर, या अन्य [[ प्रयोक्ता इंटरफ़ेस |प्रयोक्ता इंटरफ़ेस]] सम्मिलित हैं, जिसके साथ मानव प्रमाणों की खोज का मार्गदर्शन कर सकता है, जिसके विवरण संग्रहीत किए जाते हैं, और कुछ चरण कंप्यूटर द्वारा प्रदान किए जाते हैं। | ||
== सिस्टम तुलना == | == सिस्टम तुलना == | ||
{{see also| | {{see also|आश्रित प्रकार # तुलना|स्वचालित प्रमेय साबित करना#तुलना}} | ||
{| class=wikitable | {| class=wikitable | ||
|- | |- | ||
! rowspan=2 | | ! rowspan=2 | नाम !! rowspan="2" | नवीनतम संस्करण !! rowspan="2" | डवलपर्स !! rowspan="2" | कार्यान्वयन भाषा !! colspan="6" | Features | ||
|- | |- | ||
! [[Higher-order logic]] !! [[Dependent type]] | ! [[Higher-order logic|उच्च-क्रम तर्क]] !! [[Dependent type|आश्रित प्रकार]] !! छोटा कर्नल !! [[Proof automation|प्रमाण स्वचालन]] !! [[Proof by reflection|प्रतिबिंब द्वारा प्रमाण]] !! [[Code generation (compiler)|कोड जनरेशन]] | ||
|- | |- | ||
| [[ACL2]] || 8.3 || | | [[ACL2]] || 8.3 || मैट कॉफ़मैन और जे स्ट्रॉथर मूर || [[मानक लिस्प]]|| {{no}} || {{n/a|Untyped}} || {{no}} || {{yes}} || {{yes}}<ref>{{cite book|last=Hunt|first=Warren|author2=Matt Kaufmann |author3=Robert Bellarmine Krug |author4=J Moore |author5=Eric W. Smith |title=Theorem Proving in Higher Order Logics|chapter=Meta Reasoning in ACL2|series=Lecture Notes in Computer Science|year=2005|volume=3603|pages=163–178|doi=10.1007/11541868_11|isbn=978-3-540-28372-0|chapter-url=http://www.cs.utexas.edu/~moore/publications/meta-05.pdf}}</ref> || {{n/a|Already executable}} | ||
|- | |- | ||
| | | आग्डा || 2.6.2 | ||
|| | || उल्फ नॉरेल, निल्स एंडर्स डेनियलसन, और एंड्रियास एबेल (चेलमर्स और गोथेनबर्ग) ||[[हास्कल]]|| {{yes}} || {{yes}} || {{yes}} || {{no}} || {{partial}} || {{n/a|Already executable}} | ||
|- | |- | ||
| [[Albatross (programming language)|Albatross]] || 0.4 | | [[Albatross (programming language)|Albatross]] || 0.4 | ||
|| | || हेल्मुट ब्रैंडल ||[[OCaml|ओकैमल]]|| {{yes}} || {{no}} || {{yes}} || {{yes}} || {{unknown}} || {{not yet}} Implemented | ||
|- | |- | ||
| [[Coq]] || 8.15.2 || [[INRIA]] || [[OCaml]] || {{yes}} || {{yes}} || {{yes}} || {{yes}} || {{yes}} || {{yes}} | | [[Coq|सीओक्यू]] || 8.15.2 || [[INRIA|आईएनआरआईए]] || [[OCaml|ओकैमल]] || {{yes}} || {{yes}} || {{yes}} || {{yes}} || {{yes}} || {{yes}} | ||
|- | |- | ||
| [[F* (programming language)|F*]] || repository || | | [[F* (programming language)|F*]] || repository || माइक्रोसॉफ्ट रिसर्च और [[INRIA|आईएनआरआईए]]|| [[F* (programming language)|एफ*]] || {{yes}} || {{yes}} || {{no}} || {{yes}} || {{yes}}<ref>Search for "proofs by reflection": {{ArXiv|1803.06547}}</ref> || {{yes}} | ||
|- | |- | ||
| [[HOL Light]] || repository || | | [[HOL Light|एचओएल Light]] || repository || जॉन हैरिसन || [[OCaml|ओकैमल]] || {{yes}} || {{no}} || {{yes}} || {{yes}} || {{no}} || {{no}} | ||
|- | |- | ||
| [[HOL4]] || Kananaskis-13 (or repo) || | | [[HOL4|एचओएल4]] || Kananaskis-13 (or repo) || माइकल नॉरिश, कोनराड स्लिंड और अन्य || [[Standard ML|मानक एमएल]] || {{yes}} || {{no}} || {{yes}} || {{yes}} || {{no}} || {{yes}} | ||
|- | |- | ||
| [[Idris (programming language)|Idris]] || 2 0.4.0. || | | [[Idris (programming language)|Idris]] || 2 0.4.0. || एडविन ब्रैडी || इदरिस || {{yes}} || {{yes}} || {{yes}} || {{unknown}} || {{partial}} || {{yes}} | ||
|- | |- | ||
| [[Isabelle (proof assistant)|Isabelle]] || Isabelle2021 (February 2021) || | | [[Isabelle (proof assistant)|Isabelle]] || Isabelle2021 (February 2021) ||लैरी पॉलसन (कैम्ब्रिज), टोबियास निप्को (मुन्चेन) और मैकरियस वेन्ज़ेल || मानक एमएल, स्काला || {{yes}} || {{no}} || {{yes}} || {{yes}} || {{yes}} || {{yes}} | ||
|- | |- | ||
|[[Lean (proof assistant)|Lean]] | |[[Lean (proof assistant)|Lean]] | ||
|v3.4.2 (official release)<ref>{{Cite web|url=https://github.com/leanprover/lean/releases|title=Lean Theorem Prover Releases page|website=GitHub}}</ref> v3.39.1 (community release)<ref>{{Cite web|url=https://github.com/leanprover-community/lean/releases|title=Lean Community Releases Page|website=GitHub}}</ref> v4.0.0-m3 (pre-release)<ref>{{Cite web|url=https://github.com/leanprover/lean4/releases|title=Lean 4 Releases Page|website=GitHub}}</ref> | |v3.4.2 (official release)<ref>{{Cite web|url=https://github.com/leanprover/lean/releases|title=Lean Theorem Prover Releases page|website=GitHub}}</ref> v3.39.1 (community release)<ref>{{Cite web|url=https://github.com/leanprover-community/lean/releases|title=Lean Community Releases Page|website=GitHub}}</ref> v4.0.0-m3 (pre-release)<ref>{{Cite web|url=https://github.com/leanprover/lean4/releases|title=Lean 4 Releases Page|website=GitHub}}</ref> | ||
| | |लियोनार्डो डी मौरा (माइक्रोसॉफ्ट रिसर्च) | ||
|[[C++]] | |[[C++|सी++]] | ||
|{{yes}} | |{{yes}} | ||
|{{yes}} | |{{yes}} | ||
Line 44: | Line 44: | ||
|{{unknown}} | |{{unknown}} | ||
|- | |- | ||
| [[LEGO (proof assistant)|LEGO]] (not affiliated with [[Lego]]) || 1.3.1 || | | [[LEGO (proof assistant)|LEGO]] (not affiliated with [[Lego]]) || 1.3.1 || रैंडी पोलाक (एडिनबर्ग) || [[Standard ML|मानक एमएल]] || {{yes}} || {{yes}} || {{yes}} || {{no}} || {{no}} || {{no}} | ||
|- | |- | ||
| [[Mizar system|Mizar]] || 8.1.05 || [[Białystok University]] || | | [[Mizar system|Mizar]] || 8.1.05 || [[Białystok University|बेलस्टॉक विश्वविद्यालय]] || फ्री पास्कल || {{partial}} || {{yes}} || {{no}} || {{no}} || {{no}} || {{no}} | ||
|- | |- | ||
| [[NuPRL]] || 5 || [[Cornell University]] || [[Common Lisp]] || {{yes}} || {{yes}} || {{yes}} || {{yes}} || {{unknown}} || {{yes}} | | [[NuPRL]] || 5 || [[Cornell University|कॉर्नेल विश्वविद्यालय]] || [[Common Lisp|सामान्य लिस्प]] || {{yes}} || {{yes}} || {{yes}} || {{yes}} || {{unknown}} || {{yes}} | ||
|- | |- | ||
| [[Prototype Verification System|PVS]] || 6.0 || [[SRI International]] || [[Common Lisp]] || {{yes}} || {{yes}} || {{no}} || {{yes}} || {{no}} || {{unknown}} | | [[Prototype Verification System|PVS]] || 6.0 || [[SRI International|एस आर आई इंटरनेशनल]] || [[Common Lisp|सामान्य लिस्प]] || {{yes}} || {{yes}} || {{no}} || {{yes}} || {{no}} || {{unknown}} | ||
|- | |- | ||
| | | ट्वेल्फ || 1.7.1 || फ्रैंक पफेनिंग और कार्स्टन शूरमैन || [[Standard ML|मानक एमएल]] || {{yes}} || {{yes}} || {{unknown}} || {{no}} || {{no}} || {{unknown}} | ||
|} | |} | ||
* [[ACL2]] - बॉयर-मूर परंपरा में प्रोग्रामिंग भाषा, प्रथम-क्रम तार्किक सिद्धांत | * [[ACL2|एसीएल 2]] - बॉयर-मूर परंपरा में प्रोग्रामिंग भाषा, प्रथम-क्रम तार्किक सिद्धांत है और प्रमेय समर्थक अर्ताथ इंटरैक्टिव और स्वचालित मोड दोनों के साथ संलग्न होकर कार्य करता हैं। | ||
* [[Coq]] – गणितीय अभिकथनों की अभिव्यक्ति की अनुमति देता है, यंत्रवत् रूप से इन अभिकथनों के प्रमाणों की जांच करता है, औपचारिक प्रमाणों को खोजने में मदद करता है, और इसके औपचारिक विनिर्देश के रचनात्मक प्रमाण से प्रमाणित कार्यक्रम निकालता है। | * [[Coq|सीओक्यू]] – गणितीय अभिकथनों की अभिव्यक्ति की अनुमति देता है, यंत्रवत् रूप से इन अभिकथनों के प्रमाणों की जांच करता है, औपचारिक प्रमाणों को खोजने में मदद करता है, और इसके औपचारिक विनिर्देश के रचनात्मक प्रमाण से प्रमाणित कार्यक्रम निकालता है। | ||
* [[एचओएल प्रमेय समर्थक]] – उपकरणों का परिवार अंततः | * [[एचओएल प्रमेय समर्थक]] – उपकरणों का परिवार अंततः एलसीएफ थ्योरम प्रोवर से प्राप्त हुआ। इन प्रणालियों में तार्किक कोर उनकी प्रोग्रामिंग भाषा का पुस्तकालय है। प्रमेय भाषा के नए तत्वों का प्रतिनिधित्व करते हैं और केवल उन रणनीतियों के माध्यम से पेश किए जा सकते हैं जो तार्किक शुद्धता की गारंटी देते हैं। रणनीति संरचना उपयोगकर्ताओं को सिस्टम के साथ अपेक्षाकृत कम अंतःक्रियाओं के साथ महत्वपूर्ण प्रमाण प्रस्तुत करने की क्षमता देती है। परिवार के सदस्यों में सम्मिलित हैं: | ||
**[[HOL4]] – प्राथमिक वंशज , अभी भी सक्रिय विकास के अधीन है। [[मास्को एमएल]] और पॉली/एमएल दोनों के लिए | **[[HOL4|एचओएल4]] – प्राथमिक वंशज , अभी भी सक्रिय विकास के अधीन है। [[मास्को एमएल]] और पॉली/एमएल दोनों के लिए समर्थन करते हैं तथा इसमें बीएसडी-शैली का लाइसेंस भी रहता है। | ||
** [[एचओएल लाइट]] - संपन्न न्यूनतम | ** [[एचओएल लाइट]] - यह मुख्य संपन्न न्यूनतम कांटा हैं। [[ OCaml |ओकैमल]] पर आधारित रहते हैं। | ||
**प्रूफपॉवर – | **प्रूफपॉवर – स्वयं का उत्तराधिकार होने के बाद फिर से ये ओपन सोर्स पर लौट आया है। जो [[मानक एमएल]] के आधार पर उपयोग किया जाता हैं। | ||
* | * आईएमपीएस, इंटरएक्टिव मैथमैटिकल प्रूफ सिस्टम हैं।<ref>{{cite journal |last1=Farmer |first1=William M. |last2=Guttman |first2=Joshua D. |last3=Thayer |first3=F. Javier |title=IMPS: An interactive mathematical proof system |journal=Journal of Automated Reasoning |date=1993 |volume=11 |issue=2 |pages=213–248 |doi=10.1007/BF00881906 |s2cid=3084322 |access-date=22 January 2020|url=https://core.ac.uk/display/23376340}}</ref> | ||
* [[मैं इसाबेल के प्रमेय को सिद्ध करूंगा]] इंटरैक्टिव प्रमेय प्रोवर है, जो एचओएल का उत्तराधिकारी है। मुख्य कोड-बेस बीएसडी-लाइसेंस प्राप्त है, लेकिन इसाबेल वितरण विभिन्न लाइसेंसों के साथ कई ऐड-ऑन टूल को बंडल करता है। | * [[मैं इसाबेल के प्रमेय को सिद्ध करूंगा]] इंटरैक्टिव प्रमेय प्रोवर है, जो एचओएल का उत्तराधिकारी है। मुख्य कोड-बेस बीएसडी-लाइसेंस प्राप्त है, लेकिन इसाबेल वितरण विभिन्न लाइसेंसों के साथ कई ऐड-ऑन टूल को बंडल करता है। | ||
* जप (सॉफ्टवेयर) - जावा | * जप (सॉफ्टवेयर) - जावा आधारित हैं। | ||
* लीन (प्रमाण सहायक) | * लीन (प्रमाण सहायक) | ||
* [[लेगो (सबूत सहायक)]] | * [[लेगो (सबूत सहायक)|लेगो (प्रमाण सहायक)]] | ||
* [[पेंसिल]] - आगमनात्मक निर्माणों की गणना पर आधारित प्रकाश | * [[पेंसिल]] - आगमनात्मक निर्माणों की गणना पर आधारित प्रकाश प्रणाली हैं। | ||
* [[MINLOG]] – पहले क्रम के न्यूनतम तर्क पर आधारित प्रूफ | * [[MINLOG|मिनी लाॅग]] – पहले क्रम के न्यूनतम तर्क पर आधारित प्रूफ सहायक हैं। | ||
* मिज़र प्रणाली - प्रथम-क्रम तर्क पर आधारित प्रमाण सहायक, [[प्राकृतिक कटौती]] शैली में, और टार्स्की-ग्रोथेंडिक सेट | * मिज़र प्रणाली - प्रथम-क्रम तर्क पर आधारित प्रमाण सहायक, [[प्राकृतिक कटौती]] शैली में, और टार्स्की-ग्रोथेंडिक सेट सिद्धांत पर आधारित है। | ||
* [[PhoX]] – उच्च-क्रम तर्क पर आधारित प्रूफ सहायक जो एक्स्टेंसिबल है। | * [[PhoX|फो एक्स]] – उच्च-क्रम तर्क पर आधारित प्रूफ सहायक जो एक्स्टेंसिबल है। | ||
* [[प्रोटोटाइप सत्यापन प्रणाली]] (PVS) – उच्च-क्रम तर्क पर आधारित प्रमाण भाषा और | * [[प्रोटोटाइप सत्यापन प्रणाली]] (PVS) – उच्च-क्रम तर्क पर आधारित प्रमाण भाषा और प्रणाली हैं। | ||
* [[प्रमेय साबित करने की प्रणाली]] और | * [[प्रमेय साबित करने की प्रणाली|प्रमेय प्रमाणित करने की प्रणाली]] और ईटीपीएस – इंटरएक्टिव थ्योरम प्रोवर भी सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित है, लेकिन तार्किक सिद्धांत और स्वतंत्र कार्यान्वयन के स्वतंत्र क्यू0 लॉजिक पर आधारित है। | ||
== यूजर इंटरफेस == | == यूजर इंटरफेस == | ||
प्रूफ असिस्टेंट के लिए लोकप्रिय फ्रंट-एंड [[Emacs]]- आधारित प्रूफ जनरल है, जिसे [[एडिनबर्ग विश्वविद्यालय]] में विकसित किया गया है। | प्रूफ असिस्टेंट के लिए लोकप्रिय फ्रंट-एंड [[Emacs|ईमैक्स]]- आधारित प्रूफ जनरल है, जिसे [[एडिनबर्ग विश्वविद्यालय]] में विकसित किया गया है। | ||
सीओक्यू में सीओक्यूआईडीई सम्मिलित है, जो ओकैमल/[[Gtk|जीटीके]] पर आधारित है। इसाबेल में इसाबेल/[[जे संपादित करें]] सम्मिलित है, जो जेएडिट पर आधारित है और दस्तावेज उन्मुख प्रमाण प्रसंस्करण के लिए इसाबेल/स्कैला (प्रोग्रामिंग भाषा) आधारभूत संरचना है। वर्तमान समय में, इसाबेल के लिए [[विजुअल स्टूडियो कोड]] एक्सटेंशन भी मैकरियस वेन्जेल द्वारा विकसित किया गया है।<ref>{{cite web |last1=Wenzel |first1=Makarius |title=इसाबेल|url=https://marketplace.visualstudio.com/items?itemName=makarius.isabelle |access-date=2 November 2019}}</ref> | |||
== यह भी देखें == | == यह भी देखें == | ||
* | * [[स्वचालित प्रमेय साबित करना|स्वचालित प्रमेय प्रमाणित करना]] | ||
* | *[[कंप्यूटर-सहायता प्रमाण]] | ||
* | * [[औपचारिक सत्यापन]] | ||
* | * [[मेटामैथ]] | ||
* | * [[क्यूईडी घोषणापत्र]] | ||
* | * [[संतुष्टि मॉड्यूल सिद्धांत]] | ||
== टिप्पणियाँ == | == टिप्पणियाँ == | ||
Line 100: | Line 100: | ||
* [https://theoremprover-museum.github.io/ Theorem Prover Museum] | * [https://theoremprover-museum.github.io/ Theorem Prover Museum] | ||
* [http://adam.chlipala.net/cpdt/html/Intro.html "Introduction"] in ''Certified Programming with Dependent Types''. | * [http://adam.chlipala.net/cpdt/html/Intro.html "Introduction"] in ''Certified Programming with Dependent Types''. | ||
* [http://video.ias.edu/univalent/appel Introduction to the | * [http://video.ias.edu/univalent/appel Introduction to the सीओक्यू Proof Assistant] (with a general introduction to interactive theorem proving) | ||
* [http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/interactiveTheoremProvingForAgdaUsers.html Interactive Theorem Proving for Agda Users] | * [http://www.cs.swan.ac.uk/~csetzer/lectures/intertheo/07/interactiveTheoremProvingForAgdaUsers.html Interactive Theorem Proving for Agda Users] | ||
* [https://github.com/johnyf/tool_lists/blob/master/verification_synthesis.md#theorem-provers A list of theorem proving tools] | * [https://github.com/johnyf/tool_lists/blob/master/verification_synthesis.md#theorem-provers A list of theorem proving tools] | ||
Line 112: | Line 112: | ||
* [https://www.cs.cmu.edu/~fp/lfs-impl.html Specific Logical Frameworks and Implementations] | * [https://www.cs.cmu.edu/~fp/lfs-impl.html Specific Logical Frameworks and Implementations] | ||
* [[DMOZ]]: [http://www.dmoz.org/Science/Math/Logic_and_Foundations/Computational_Logic/Logical_Frameworks/ Science: Math: Logic and Foundations: Computational Logic: Logical Frameworks] | * [[DMOZ]]: [http://www.dmoz.org/Science/Math/Logic_and_Foundations/Computational_Logic/Logical_Frameworks/ Science: Math: Logic and Foundations: Computational Logic: Logical Frameworks] | ||
[[de:Maschinengestütztes Beweisen]] | [[de:Maschinengestütztes Beweisen]] | ||
[[Category:Articles with hatnote templates targeting a nonexistent page]] | |||
[[Category: | |||
[[Category:Created On 02/03/2023]] | [[Category:Created On 02/03/2023]] | ||
[[Category:Lua-based templates]] | |||
[[Category:Machine Translated Page]] | |||
[[Category:Pages with script errors]] | |||
[[Category:Short description with empty Wikidata description]] | |||
[[Category:Templates Vigyan Ready]] | |||
[[Category:Templates that add a tracking category]] | |||
[[Category:Templates that generate short descriptions]] | |||
[[Category:Templates using TemplateData]] | |||
[[Category:तर्क तकनीक]] | |||
[[Category:सबूत सहायक| सबूत सहायक ]] | |||
[[Category:स्वचालित प्रमेय साबित करना]] |
Latest revision as of 15:21, 14 September 2023
कंप्यूटर विज्ञान और गणितीय तर्क में, प्रमाण सहायक या इंटरैक्टिव प्रमेय प्रोवर मानव-मशीन सहयोग से औपचारिक प्रमाण के विकास में सहायता के लिए सॉफ्टवेयर उपकरण है। इसमें कुछ प्रकार के इंटरएक्टिव प्रूफ एडिटर, या अन्य प्रयोक्ता इंटरफ़ेस सम्मिलित हैं, जिसके साथ मानव प्रमाणों की खोज का मार्गदर्शन कर सकता है, जिसके विवरण संग्रहीत किए जाते हैं, और कुछ चरण कंप्यूटर द्वारा प्रदान किए जाते हैं।
सिस्टम तुलना
नाम | नवीनतम संस्करण | डवलपर्स | कार्यान्वयन भाषा | Features | |||||
---|---|---|---|---|---|---|---|---|---|
उच्च-क्रम तर्क | आश्रित प्रकार | छोटा कर्नल | प्रमाण स्वचालन | प्रतिबिंब द्वारा प्रमाण | कोड जनरेशन | ||||
ACL2 | 8.3 | मैट कॉफ़मैन और जे स्ट्रॉथर मूर | मानक लिस्प | No | Untyped | No | Yes | Yes[1] | Already executable |
आग्डा | 2.6.2 | उल्फ नॉरेल, निल्स एंडर्स डेनियलसन, और एंड्रियास एबेल (चेलमर्स और गोथेनबर्ग) | हास्कल | Yes | Yes | Yes | No | Partial | Already executable |
Albatross | 0.4 | हेल्मुट ब्रैंडल | ओकैमल | Yes | No | Yes | Yes | Unknown | Not yet Implemented |
सीओक्यू | 8.15.2 | आईएनआरआईए | ओकैमल | Yes | Yes | Yes | Yes | Yes | Yes |
F* | repository | माइक्रोसॉफ्ट रिसर्च और आईएनआरआईए | एफ* | Yes | Yes | No | Yes | Yes[2] | Yes |
एचओएल Light | repository | जॉन हैरिसन | ओकैमल | Yes | No | Yes | Yes | No | No |
एचओएल4 | Kananaskis-13 (or repo) | माइकल नॉरिश, कोनराड स्लिंड और अन्य | मानक एमएल | Yes | No | Yes | Yes | No | Yes |
Idris | 2 0.4.0. | एडविन ब्रैडी | इदरिस | Yes | Yes | Yes | Unknown | Partial | Yes |
Isabelle | Isabelle2021 (February 2021) | लैरी पॉलसन (कैम्ब्रिज), टोबियास निप्को (मुन्चेन) और मैकरियस वेन्ज़ेल | मानक एमएल, स्काला | Yes | No | Yes | Yes | Yes | Yes |
Lean | v3.4.2 (official release)[3] v3.39.1 (community release)[4] v4.0.0-m3 (pre-release)[5] | लियोनार्डो डी मौरा (माइक्रोसॉफ्ट रिसर्च) | सी++ | Yes | Yes | Yes | Yes | Yes | Unknown |
LEGO (not affiliated with Lego) | 1.3.1 | रैंडी पोलाक (एडिनबर्ग) | मानक एमएल | Yes | Yes | Yes | No | No | No |
Mizar | 8.1.05 | बेलस्टॉक विश्वविद्यालय | फ्री पास्कल | Partial | Yes | No | No | No | No |
NuPRL | 5 | कॉर्नेल विश्वविद्यालय | सामान्य लिस्प | Yes | Yes | Yes | Yes | Unknown | Yes |
PVS | 6.0 | एस आर आई इंटरनेशनल | सामान्य लिस्प | Yes | Yes | No | Yes | No | Unknown |
ट्वेल्फ | 1.7.1 | फ्रैंक पफेनिंग और कार्स्टन शूरमैन | मानक एमएल | Yes | Yes | Unknown | No | No | Unknown |
- एसीएल 2 - बॉयर-मूर परंपरा में प्रोग्रामिंग भाषा, प्रथम-क्रम तार्किक सिद्धांत है और प्रमेय समर्थक अर्ताथ इंटरैक्टिव और स्वचालित मोड दोनों के साथ संलग्न होकर कार्य करता हैं।
- सीओक्यू – गणितीय अभिकथनों की अभिव्यक्ति की अनुमति देता है, यंत्रवत् रूप से इन अभिकथनों के प्रमाणों की जांच करता है, औपचारिक प्रमाणों को खोजने में मदद करता है, और इसके औपचारिक विनिर्देश के रचनात्मक प्रमाण से प्रमाणित कार्यक्रम निकालता है।
- एचओएल प्रमेय समर्थक – उपकरणों का परिवार अंततः एलसीएफ थ्योरम प्रोवर से प्राप्त हुआ। इन प्रणालियों में तार्किक कोर उनकी प्रोग्रामिंग भाषा का पुस्तकालय है। प्रमेय भाषा के नए तत्वों का प्रतिनिधित्व करते हैं और केवल उन रणनीतियों के माध्यम से पेश किए जा सकते हैं जो तार्किक शुद्धता की गारंटी देते हैं। रणनीति संरचना उपयोगकर्ताओं को सिस्टम के साथ अपेक्षाकृत कम अंतःक्रियाओं के साथ महत्वपूर्ण प्रमाण प्रस्तुत करने की क्षमता देती है। परिवार के सदस्यों में सम्मिलित हैं:
- एचओएल4 – प्राथमिक वंशज , अभी भी सक्रिय विकास के अधीन है। मास्को एमएल और पॉली/एमएल दोनों के लिए समर्थन करते हैं तथा इसमें बीएसडी-शैली का लाइसेंस भी रहता है।
- एचओएल लाइट - यह मुख्य संपन्न न्यूनतम कांटा हैं। ओकैमल पर आधारित रहते हैं।
- प्रूफपॉवर – स्वयं का उत्तराधिकार होने के बाद फिर से ये ओपन सोर्स पर लौट आया है। जो मानक एमएल के आधार पर उपयोग किया जाता हैं।
- आईएमपीएस, इंटरएक्टिव मैथमैटिकल प्रूफ सिस्टम हैं।[6]
- मैं इसाबेल के प्रमेय को सिद्ध करूंगा इंटरैक्टिव प्रमेय प्रोवर है, जो एचओएल का उत्तराधिकारी है। मुख्य कोड-बेस बीएसडी-लाइसेंस प्राप्त है, लेकिन इसाबेल वितरण विभिन्न लाइसेंसों के साथ कई ऐड-ऑन टूल को बंडल करता है।
- जप (सॉफ्टवेयर) - जावा आधारित हैं।
- लीन (प्रमाण सहायक)
- लेगो (प्रमाण सहायक)
- पेंसिल - आगमनात्मक निर्माणों की गणना पर आधारित प्रकाश प्रणाली हैं।
- मिनी लाॅग – पहले क्रम के न्यूनतम तर्क पर आधारित प्रूफ सहायक हैं।
- मिज़र प्रणाली - प्रथम-क्रम तर्क पर आधारित प्रमाण सहायक, प्राकृतिक कटौती शैली में, और टार्स्की-ग्रोथेंडिक सेट सिद्धांत पर आधारित है।
- फो एक्स – उच्च-क्रम तर्क पर आधारित प्रूफ सहायक जो एक्स्टेंसिबल है।
- प्रोटोटाइप सत्यापन प्रणाली (PVS) – उच्च-क्रम तर्क पर आधारित प्रमाण भाषा और प्रणाली हैं।
- प्रमेय प्रमाणित करने की प्रणाली और ईटीपीएस – इंटरएक्टिव थ्योरम प्रोवर भी सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित है, लेकिन तार्किक सिद्धांत और स्वतंत्र कार्यान्वयन के स्वतंत्र क्यू0 लॉजिक पर आधारित है।
यूजर इंटरफेस
प्रूफ असिस्टेंट के लिए लोकप्रिय फ्रंट-एंड ईमैक्स- आधारित प्रूफ जनरल है, जिसे एडिनबर्ग विश्वविद्यालय में विकसित किया गया है।
सीओक्यू में सीओक्यूआईडीई सम्मिलित है, जो ओकैमल/जीटीके पर आधारित है। इसाबेल में इसाबेल/जे संपादित करें सम्मिलित है, जो जेएडिट पर आधारित है और दस्तावेज उन्मुख प्रमाण प्रसंस्करण के लिए इसाबेल/स्कैला (प्रोग्रामिंग भाषा) आधारभूत संरचना है। वर्तमान समय में, इसाबेल के लिए विजुअल स्टूडियो कोड एक्सटेंशन भी मैकरियस वेन्जेल द्वारा विकसित किया गया है।[7]
यह भी देखें
- स्वचालित प्रमेय प्रमाणित करना
- कंप्यूटर-सहायता प्रमाण
- औपचारिक सत्यापन
- मेटामैथ
- क्यूईडी घोषणापत्र
- संतुष्टि मॉड्यूल सिद्धांत
टिप्पणियाँ
- ↑ Hunt, Warren; Matt Kaufmann; Robert Bellarmine Krug; J Moore; Eric W. Smith (2005). "Meta Reasoning in ACL2" (PDF). Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science. Vol. 3603. pp. 163–178. doi:10.1007/11541868_11. ISBN 978-3-540-28372-0.
- ↑ Search for "proofs by reflection": arXiv:1803.06547
- ↑ "Lean Theorem Prover Releases page". GitHub.
- ↑ "Lean Community Releases Page". GitHub.
- ↑ "Lean 4 Releases Page". GitHub.
- ↑ Farmer, William M.; Guttman, Joshua D.; Thayer, F. Javier (1993). "IMPS: An interactive mathematical proof system". Journal of Automated Reasoning. 11 (2): 213–248. doi:10.1007/BF00881906. S2CID 3084322. Retrieved 22 January 2020.
- ↑ Wenzel, Makarius. "इसाबेल". Retrieved 2 November 2019.
संदर्भ
- Barendregt, Henk; Geuvers, Herman (2001). "18. Proof-assistants using Dependent Type Systems" (PDF). In Robinson, Alan J.A.; Voronkov, Andrei (eds.). Handbook of Automated Reasoning. Vol. 2. Elsevier. pp. 1149–. ISBN 978-0-444-50812-6. Archived from the original (PDF) on 2007-07-27.
- Pfenning, Frank. "17. Logical frameworks" (PDF). Handbook vol 2 2001. pp. 1065–1148.
- Pfenning, Frank (1996). "The practice of logical frameworks". In Kirchner, H. (ed.). Trees in Algebra and Programming — CAAP '96. Lecture Notes in Computer Science. Vol. 1059. Springer. pp. 119–134. doi:10.1007/3-540-61064-2_33. ISBN 3-540-61064-2.
- Constable, Robert L. (1998). "X. Types in computer science, philosophy and logic". In Buss, S.R. (ed.). Handbook of Proof Theory. Studies in Logic. Vol. 137. Elsevier. pp. 683–786. ISBN 978-0-08-053318-6.
- Geuvers, H. (February 2009). "Proof assistants: History, ideas and future". Sādhanā. 34 (1): 3–25. doi:10.1007/s12046-009-0001-5. S2CID 14827467.
- Wiedijk, Freek (2005). "The Seventeen Provers of the World" (PDF). Radboud University Nijmegen.
बाहरी संबंध
- Theorem Prover Museum
- "Introduction" in Certified Programming with Dependent Types.
- Introduction to the सीओक्यू Proof Assistant (with a general introduction to interactive theorem proving)
- Interactive Theorem Proving for Agda Users
- A list of theorem proving tools
- Catalogues
- Digital Math by Category: Tactic Provers
- Automated Deduction Systems and Groups
- Theorem Proving and Automated Reasoning Systems
- Database of Existing Mechanized Reasoning Systems
- NuPRL: Other Systems
- Specific Logical Frameworks and Implementations
- DMOZ: Science: Math: Logic and Foundations: Computational Logic: Logical Frameworks