प्रमाण सहायक: Difference between revisions
From Vigyanwiki
(Created page with "{{Short description|Software tool to assist with the development of formal proofs by human-machine collaboration}} {{for|verification in computer science|formal verification}}...") |
No edit summary |
||
| Line 2: | Line 2: | ||
{{for|verification in computer science|formal verification}} | {{for|verification in computer science|formal verification}} | ||
{{for|the academic conference|Interactive Theorem Proving (conference)}} | {{for|the academic conference|Interactive Theorem Proving (conference)}} | ||
{{distinguish|Interactive proof system}} | {{distinguish|Interactive proof system}}[[Image:CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png|thumb|CoqIDE में इंटरएक्टिव प्रूफ सत्र, बाईं ओर प्रूफ स्क्रिप्ट और दाईं ओर प्रूफ स्टेट दिखा रहा है।]][[[[कंप्यूटर]] विज्ञान]] और [[गणितीय तर्क]] में, सबूत सहायक या इंटरैक्टिव प्रमेय प्रोवर मानव-मशीन सहयोग से औपचारिक सबूत के विकास में सहायता के लिए सॉफ्टवेयर उपकरण है। इसमें कुछ प्रकार के इंटरएक्टिव प्रूफ एडिटर, या अन्य [[ प्रयोक्ता इंटरफ़ेस |प्रयोक्ता इंटरफ़ेस]] शामिल हैं, जिसके साथ मानव सबूतों की खोज का मार्गदर्शन कर सकता है, जिसके विवरण संग्रहीत किए जाते हैं, और कुछ चरण कंप्यूटर द्वारा प्रदान किए जाते हैं। | ||
== सिस्टम तुलना == | |||
{{see also|Dependent type#Comparison|Automated theorem proving#Comparison}} | |||
{| class=wikitable | {| class=wikitable | ||
|- | |- | ||
| Line 57: | Line 54: | ||
| [[Twelf]] || 1.7.1 || [[Frank Pfenning]] and [[Carsten Schürmann]] || [[Standard ML]] || {{yes}} || {{yes}} || {{unknown}} || {{no}} || {{no}} || {{unknown}} | | [[Twelf]] || 1.7.1 || [[Frank Pfenning]] and [[Carsten Schürmann]] || [[Standard ML]] || {{yes}} || {{yes}} || {{unknown}} || {{no}} || {{no}} || {{unknown}} | ||
|} | |} | ||
* [[ACL2]] - बॉयर-मूर परंपरा में | * [[ACL2]] - बॉयर-मूर परंपरा में प्रोग्रामिंग भाषा, प्रथम-क्रम तार्किक सिद्धांत, और प्रमेय समर्थक (इंटरैक्टिव और स्वचालित मोड दोनों के साथ)। | ||
* [[Coq]] – गणितीय अभिकथनों की अभिव्यक्ति की अनुमति देता है, यंत्रवत् रूप से इन अभिकथनों के प्रमाणों की जांच करता है, औपचारिक प्रमाणों को खोजने में मदद करता है, और इसके औपचारिक विनिर्देश के रचनात्मक प्रमाण से | * [[Coq]] – गणितीय अभिकथनों की अभिव्यक्ति की अनुमति देता है, यंत्रवत् रूप से इन अभिकथनों के प्रमाणों की जांच करता है, औपचारिक प्रमाणों को खोजने में मदद करता है, और इसके औपचारिक विनिर्देश के रचनात्मक प्रमाण से प्रमाणित कार्यक्रम निकालता है। | ||
* [[एचओएल प्रमेय समर्थक]] – उपकरणों का | * [[एचओएल प्रमेय समर्थक]] – उपकरणों का परिवार अंततः LCF थ्योरम प्रोवर से प्राप्त हुआ। इन प्रणालियों में तार्किक कोर उनकी प्रोग्रामिंग भाषा का पुस्तकालय है। प्रमेय भाषा के नए तत्वों का प्रतिनिधित्व करते हैं और केवल उन रणनीतियों के माध्यम से पेश किए जा सकते हैं जो तार्किक शुद्धता की गारंटी देते हैं। रणनीति संरचना उपयोगकर्ताओं को सिस्टम के साथ अपेक्षाकृत कम अंतःक्रियाओं के साथ महत्वपूर्ण प्रमाण प्रस्तुत करने की क्षमता देती है। परिवार के सदस्यों में शामिल हैं: | ||
**[[HOL4]] – प्राथमिक वंशज , अभी भी सक्रिय विकास के अधीन है। [[मास्को एमएल]] और पॉली/एमएल दोनों के लिए समर्थन। बीएसडी-शैली का लाइसेंस है। | **[[HOL4]] – प्राथमिक वंशज , अभी भी सक्रिय विकास के अधीन है। [[मास्को एमएल]] और पॉली/एमएल दोनों के लिए समर्थन। बीएसडी-शैली का लाइसेंस है। | ||
** [[एचओएल लाइट]] - | ** [[एचओएल लाइट]] - संपन्न न्यूनतम कांटा। [[ OCaml |OCaml]] आधारित। | ||
**प्रूफपॉवर – मालिकाना हो गया, फिर ओपन सोर्स पर लौट आया। [[मानक एमएल]] के आधार पर। | **प्रूफपॉवर – मालिकाना हो गया, फिर ओपन सोर्स पर लौट आया। [[मानक एमएल]] के आधार पर। | ||
* IMPS, | * IMPS, इंटरएक्टिव मैथमैटिकल प्रूफ सिस्टम<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) – उच्च-क्रम तर्क पर आधारित प्रमाण भाषा और प्रणाली। | ||
* [[प्रमेय साबित करने की प्रणाली]] और ETPS – इंटरएक्टिव थ्योरम प्रोवर भी सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित है, लेकिन तार्किक सिद्धांत और स्वतंत्र कार्यान्वयन के | * [[प्रमेय साबित करने की प्रणाली]] और ETPS – इंटरएक्टिव थ्योरम प्रोवर भी सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित है, लेकिन तार्किक सिद्धांत और स्वतंत्र कार्यान्वयन के स्वतंत्र Q0 लॉजिक पर आधारित है। | ||
== यूजर इंटरफेस == | == यूजर इंटरफेस == | ||
प्रूफ असिस्टेंट के लिए | प्रूफ असिस्टेंट के लिए लोकप्रिय फ्रंट-एंड [[Emacs]]- आधारित प्रूफ जनरल है, जिसे [[एडिनबर्ग विश्वविद्यालय]] में विकसित किया गया है। | ||
Coq में CoqIDE शामिल है, जो OCaml/[[Gtk]] पर आधारित है। इसाबेल में इसाबेल/[[जे संपादित करें]] शामिल है, जो जेएडिट पर आधारित है और दस्तावेज उन्मुख सबूत प्रसंस्करण के लिए इसाबेल/स्कैला (प्रोग्रामिंग भाषा) आधारभूत संरचना है। अभी हाल ही में, इसाबेल के लिए [[विजुअल स्टूडियो कोड]] एक्सटेंशन भी मैकरियस वेन्जेल द्वारा विकसित किया गया है।<ref>{{cite web |last1=Wenzel |first1=Makarius |title=इसाबेल|url=https://marketplace.visualstudio.com/items?itemName=makarius.isabelle |access-date=2 November 2019}}</ref> | |||
== यह भी देखें == | == यह भी देखें == | ||
* {{annotated link|Automated theorem proving}} | * {{annotated link|Automated theorem proving}} | ||
| Line 103: | Line 98: | ||
== बाहरी संबंध == | == बाहरी संबंध == | ||
* [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''. | ||
Revision as of 23:10, 7 March 2023
[[कंप्यूटर विज्ञान]] और गणितीय तर्क में, सबूत सहायक या इंटरैक्टिव प्रमेय प्रोवर मानव-मशीन सहयोग से औपचारिक सबूत के विकास में सहायता के लिए सॉफ्टवेयर उपकरण है। इसमें कुछ प्रकार के इंटरएक्टिव प्रूफ एडिटर, या अन्य प्रयोक्ता इंटरफ़ेस शामिल हैं, जिसके साथ मानव सबूतों की खोज का मार्गदर्शन कर सकता है, जिसके विवरण संग्रहीत किए जाते हैं, और कुछ चरण कंप्यूटर द्वारा प्रदान किए जाते हैं।
सिस्टम तुलना
| Name | Latest version | Developer(s) | Implementation language | Features | |||||
|---|---|---|---|---|---|---|---|---|---|
| Higher-order logic | Dependent types | Small kernel | Proof automation | Proof by reflection | Code generation | ||||
| ACL2 | 8.3 | Matt Kaufmann and J Strother Moore | Common Lisp | No | Untyped | No | Yes | Yes[1] | Already executable |
| Agda | 2.6.2 | Ulf Norell, Nils Anders Danielsson, and Andreas Abel (Chalmers and Gothenburg) | Haskell | Yes | Yes | Yes | No | Partial | Already executable |
| Albatross | 0.4 | Helmut Brandl | OCaml | Yes | No | Yes | Yes | Unknown | Not yet Implemented |
| Coq | 8.15.2 | INRIA | OCaml | Yes | Yes | Yes | Yes | Yes | Yes |
| F* | repository | Microsoft Research and INRIA | F* | Yes | Yes | No | Yes | Yes[2] | Yes |
| HOL Light | repository | John Harrison | OCaml | Yes | No | Yes | Yes | No | No |
| HOL4 | Kananaskis-13 (or repo) | Michael Norrish, Konrad Slind, and others | Standard ML | Yes | No | Yes | Yes | No | Yes |
| Idris | 2 0.4.0. | Edwin Brady | Idris | Yes | Yes | Yes | Unknown | Partial | Yes |
| Isabelle | Isabelle2021 (February 2021) | Larry Paulson (Cambridge), Tobias Nipkow (München) and Makarius Wenzel | Standard ML, Scala | 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] | Leonardo de Moura (Microsoft Research) | C++ | Yes | Yes | Yes | Yes | Yes | Unknown |
| LEGO (not affiliated with Lego) | 1.3.1 | Randy Pollack (Edinburgh) | Standard ML | Yes | Yes | Yes | No | No | No |
| Mizar | 8.1.05 | Białystok University | Free Pascal | Partial | Yes | No | No | No | No |
| NuPRL | 5 | Cornell University | Common Lisp | Yes | Yes | Yes | Yes | Unknown | Yes |
| PVS | 6.0 | SRI International | Common Lisp | Yes | Yes | No | Yes | No | Unknown |
| Twelf | 1.7.1 | Frank Pfenning and Carsten Schürmann | Standard ML | Yes | Yes | Unknown | No | No | Unknown |
- ACL2 - बॉयर-मूर परंपरा में प्रोग्रामिंग भाषा, प्रथम-क्रम तार्किक सिद्धांत, और प्रमेय समर्थक (इंटरैक्टिव और स्वचालित मोड दोनों के साथ)।
- Coq – गणितीय अभिकथनों की अभिव्यक्ति की अनुमति देता है, यंत्रवत् रूप से इन अभिकथनों के प्रमाणों की जांच करता है, औपचारिक प्रमाणों को खोजने में मदद करता है, और इसके औपचारिक विनिर्देश के रचनात्मक प्रमाण से प्रमाणित कार्यक्रम निकालता है।
- एचओएल प्रमेय समर्थक – उपकरणों का परिवार अंततः LCF थ्योरम प्रोवर से प्राप्त हुआ। इन प्रणालियों में तार्किक कोर उनकी प्रोग्रामिंग भाषा का पुस्तकालय है। प्रमेय भाषा के नए तत्वों का प्रतिनिधित्व करते हैं और केवल उन रणनीतियों के माध्यम से पेश किए जा सकते हैं जो तार्किक शुद्धता की गारंटी देते हैं। रणनीति संरचना उपयोगकर्ताओं को सिस्टम के साथ अपेक्षाकृत कम अंतःक्रियाओं के साथ महत्वपूर्ण प्रमाण प्रस्तुत करने की क्षमता देती है। परिवार के सदस्यों में शामिल हैं:
- HOL4 – प्राथमिक वंशज , अभी भी सक्रिय विकास के अधीन है। मास्को एमएल और पॉली/एमएल दोनों के लिए समर्थन। बीएसडी-शैली का लाइसेंस है।
- एचओएल लाइट - संपन्न न्यूनतम कांटा। OCaml आधारित।
- प्रूफपॉवर – मालिकाना हो गया, फिर ओपन सोर्स पर लौट आया। मानक एमएल के आधार पर।
- IMPS, इंटरएक्टिव मैथमैटिकल प्रूफ सिस्टम[6]
- मैं इसाबेल के प्रमेय को सिद्ध करूंगा इंटरैक्टिव प्रमेय प्रोवर है, जो एचओएल का उत्तराधिकारी है। मुख्य कोड-बेस बीएसडी-लाइसेंस प्राप्त है, लेकिन इसाबेल वितरण विभिन्न लाइसेंसों के साथ कई ऐड-ऑन टूल को बंडल करता है।
- जप (सॉफ्टवेयर) - जावा आधारित।
- लीन (प्रमाण सहायक)
- लेगो (सबूत सहायक)
- पेंसिल - आगमनात्मक निर्माणों की गणना पर आधारित प्रकाश प्रणाली।
- MINLOG – पहले क्रम के न्यूनतम तर्क पर आधारित प्रूफ सहायक।
- मिज़र प्रणाली - प्रथम-क्रम तर्क पर आधारित प्रमाण सहायक, प्राकृतिक कटौती शैली में, और टार्स्की-ग्रोथेंडिक सेट सिद्धांत।
- PhoX – उच्च-क्रम तर्क पर आधारित प्रूफ सहायक जो एक्स्टेंसिबल है।
- प्रोटोटाइप सत्यापन प्रणाली (PVS) – उच्च-क्रम तर्क पर आधारित प्रमाण भाषा और प्रणाली।
- प्रमेय साबित करने की प्रणाली और ETPS – इंटरएक्टिव थ्योरम प्रोवर भी सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित है, लेकिन तार्किक सिद्धांत और स्वतंत्र कार्यान्वयन के स्वतंत्र Q0 लॉजिक पर आधारित है।
यूजर इंटरफेस
प्रूफ असिस्टेंट के लिए लोकप्रिय फ्रंट-एंड Emacs- आधारित प्रूफ जनरल है, जिसे एडिनबर्ग विश्वविद्यालय में विकसित किया गया है।
Coq में CoqIDE शामिल है, जो OCaml/Gtk पर आधारित है। इसाबेल में इसाबेल/जे संपादित करें शामिल है, जो जेएडिट पर आधारित है और दस्तावेज उन्मुख सबूत प्रसंस्करण के लिए इसाबेल/स्कैला (प्रोग्रामिंग भाषा) आधारभूत संरचना है। अभी हाल ही में, इसाबेल के लिए विजुअल स्टूडियो कोड एक्सटेंशन भी मैकरियस वेन्जेल द्वारा विकसित किया गया है।[7]
यह भी देखें
- Automated theorem proving
- Computer-assisted proof
- Formal verification
- Metamath
- QED manifesto
- Satisfiability modulo theories
टिप्पणियाँ
- ↑ 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 Coq 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
