प्रमाण सहायक
From Vigyanwiki
कंप्यूटर विज्ञान और गणितीय तर्क में, प्रमाण सहायक या इंटरैक्टिव प्रमेय प्रोवर मानव-मशीन सहयोग से औपचारिक प्रमाण के विकास में सहायता के लिए सॉफ्टवेयर उपकरण है। इसमें कुछ प्रकार के इंटरएक्टिव प्रूफ एडिटर, या अन्य प्रयोक्ता इंटरफ़ेस सम्मिलित हैं, जिसके साथ मानव प्रमाणों की खोज का मार्गदर्शन कर सकता है, जिसके विवरण संग्रहीत किए जाते हैं, और कुछ चरण कंप्यूटर द्वारा प्रदान किए जाते हैं।
सिस्टम तुलना
| नाम | नवीनतम संस्करण | डवलपर्स | कार्यान्वयन भाषा | 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
