प्रमाण सहायक

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 Un­known 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 Un­known 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 Un­known
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 Un­known Yes
PVS 6.0 एस आर आई इंटरनेशनल सामान्य लिस्प Yes Yes No Yes No Un­known
ट्वेल्फ 1.7.1 फ्रैंक पफेनिंग और कार्स्टन शूरमैन मानक एमएल Yes Yes Un­known No No Un­known
  • एसीएल 2 - बॉयर-मूर परंपरा में प्रोग्रामिंग भाषा, प्रथम-क्रम तार्किक सिद्धांत है और प्रमेय समर्थक अर्ताथ इंटरैक्टिव और स्वचालित मोड दोनों के साथ संलग्न होकर कार्य करता हैं।
  • सीओक्यू – गणितीय अभिकथनों की अभिव्यक्ति की अनुमति देता है, यंत्रवत् रूप से इन अभिकथनों के प्रमाणों की जांच करता है, औपचारिक प्रमाणों को खोजने में मदद करता है, और इसके औपचारिक विनिर्देश के रचनात्मक प्रमाण से प्रमाणित कार्यक्रम निकालता है।
  • एचओएल प्रमेय समर्थक – उपकरणों का परिवार अंततः एलसीएफ थ्योरम प्रोवर से प्राप्त हुआ। इन प्रणालियों में तार्किक कोर उनकी प्रोग्रामिंग भाषा का पुस्तकालय है। प्रमेय भाषा के नए तत्वों का प्रतिनिधित्व करते हैं और केवल उन रणनीतियों के माध्यम से पेश किए जा सकते हैं जो तार्किक शुद्धता की गारंटी देते हैं। रणनीति संरचना उपयोगकर्ताओं को सिस्टम के साथ अपेक्षाकृत कम अंतःक्रियाओं के साथ महत्वपूर्ण प्रमाण प्रस्तुत करने की क्षमता देती है। परिवार के सदस्यों में सम्मिलित हैं:
    • एचओएल4 – प्राथमिक वंशज , अभी भी सक्रिय विकास के अधीन है। मास्को एमएल और पॉली/एमएल दोनों के लिए समर्थन करते हैं तथा इसमें बीएसडी-शैली का लाइसेंस भी रहता है।
    • एचओएल लाइट - यह मुख्य संपन्न न्यूनतम कांटा हैं। ओकैमल पर आधारित रहते हैं।
    • प्रूफपॉवर – स्वयं का उत्तराधिकार होने के बाद फिर से ये ओपन सोर्स पर लौट आया है। जो मानक एमएल के आधार पर उपयोग किया जाता हैं।
  • आईएमपीएस, इंटरएक्टिव मैथमैटिकल प्रूफ सिस्टम हैं।[6]
  • मैं इसाबेल के प्रमेय को सिद्ध करूंगा इंटरैक्टिव प्रमेय प्रोवर है, जो एचओएल का उत्तराधिकारी है। मुख्य कोड-बेस बीएसडी-लाइसेंस प्राप्त है, लेकिन इसाबेल वितरण विभिन्न लाइसेंसों के साथ कई ऐड-ऑन टूल को बंडल करता है।
  • जप (सॉफ्टवेयर) - जावा आधारित हैं।
  • लीन (प्रमाण सहायक)
  • लेगो (प्रमाण सहायक)
  • पेंसिल - आगमनात्मक निर्माणों की गणना पर आधारित प्रकाश प्रणाली हैं।
  • मिनी लाॅग – पहले क्रम के न्यूनतम तर्क पर आधारित प्रूफ सहायक हैं।
  • मिज़र प्रणाली - प्रथम-क्रम तर्क पर आधारित प्रमाण सहायक, प्राकृतिक कटौती शैली में, और टार्स्की-ग्रोथेंडिक सेट सिद्धांत पर आधारित है।
  • फो एक्स – उच्च-क्रम तर्क पर आधारित प्रूफ सहायक जो एक्स्टेंसिबल है।
  • प्रोटोटाइप सत्यापन प्रणाली (PVS) – उच्च-क्रम तर्क पर आधारित प्रमाण भाषा और प्रणाली हैं।
  • प्रमेय प्रमाणित करने की प्रणाली और ईटीपीएस – इंटरएक्टिव थ्योरम प्रोवर भी सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित है, लेकिन तार्किक सिद्धांत और स्वतंत्र कार्यान्वयन के स्वतंत्र क्यू0 लॉजिक पर आधारित है।

यूजर इंटरफेस

प्रूफ असिस्टेंट के लिए लोकप्रिय फ्रंट-एंड ईमैक्स- आधारित प्रूफ जनरल है, जिसे एडिनबर्ग विश्वविद्यालय में विकसित किया गया है।

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

यह भी देखें

टिप्पणियाँ

  1. 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.
  2. Search for "proofs by reflection": arXiv:1803.06547
  3. "Lean Theorem Prover Releases page". GitHub.
  4. "Lean Community Releases Page". GitHub.
  5. "Lean 4 Releases Page". GitHub.
  6. 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.
  7. Wenzel, Makarius. "इसाबेल". Retrieved 2 November 2019.


संदर्भ


बाहरी संबंध

Catalogues