प्रमाण सहायक: Difference between revisions

Revision as of 23:54, 7 March 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

[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.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

@@ Line 1: / Line 1: @@
 {{Short description|Software tool to assist with the development of formal proofs by human-machine collaboration}}
-{{for|verification in computer science|formal verification}}
+{{for|कंप्यूटर विज्ञान में सत्यापन|औपचारिक सत्यापन}}
-{{for|the academic conference|Interactive Theorem Proving (conference)}}
+{{for|शैक्षणिक सम्मेलन|इंटरएक्टिव प्रमेय साबित करना (सम्मेलन)}}
-{{distinguish|Interactive proof system}}[[Image:CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png|thumb|CoqIDE में इंटरएक्टिव प्रूफ सत्र, बाईं ओर प्रूफ स्क्रिप्ट और दाईं ओर प्रूफ स्टेट दिखा रहा है।]][[[[कंप्यूटर]] विज्ञान]] और [[गणितीय तर्क]] में, सबूत सहायक या इंटरैक्टिव प्रमेय प्रोवर मानव-मशीन सहयोग से औपचारिक सबूत के विकास में सहायता के लिए सॉफ्टवेयर उपकरण है। इसमें कुछ प्रकार के इंटरएक्टिव प्रूफ एडिटर, या अन्य [[ प्रयोक्ता इंटरफ़ेस |प्रयोक्ता इंटरफ़ेस]] शामिल हैं, जिसके साथ मानव सबूतों की खोज का मार्गदर्शन कर सकता है, जिसके विवरण संग्रहीत किए जाते हैं, और कुछ चरण कंप्यूटर द्वारा प्रदान किए जाते हैं।
+{{distinguish|इंटरएक्टिव प्रूफ सिस्टम}}[[Image:CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png|thumb|सीओक्यूआईडीई में इंटरएक्टिव प्रूफ सत्र, बाईं ओर प्रूफ स्क्रिप्ट और दाईं ओर प्रूफ स्टेट दिखा रहा है।]][[कंप्यूटर]] विज्ञान और [[गणितीय तर्क]] में, '''प्रमाण सहायक''' या इंटरैक्टिव प्रमेय प्रोवर मानव-मशीन सहयोग से औपचारिक प्रमाण के विकास में सहायता के लिए सॉफ्टवेयर उपकरण है। इसमें कुछ प्रकार के इंटरएक्टिव प्रूफ एडिटर, या अन्य [[ प्रयोक्ता इंटरफ़ेस |प्रयोक्ता इंटरफ़ेस]] सम्मिलित हैं, जिसके साथ मानव प्रमाणों की खोज का मार्गदर्शन कर सकता है, जिसके विवरण संग्रहीत किए जाते हैं, और कुछ चरण कंप्यूटर द्वारा प्रदान किए जाते हैं।
 == सिस्टम तुलना ==
-{{see also|Dependent type#Comparison|Automated theorem proving#Comparison}}
+{{see also|आश्रित प्रकार # तुलना|स्वचालित प्रमेय साबित करना#तुलना}}
 {| class=wikitable
 |-
-! rowspan=2 | Name !! rowspan=2 | Latest version !! rowspan=2 | Developer(s) !! rowspan=2 | Implementation language !! colspan=6 | Features
+! rowspan=2 | नाम !! rowspan="2" | नवीनतम संस्करण !! rowspan="2" | डवलपर्स !! rowspan="2" | कार्यान्वयन भाषा !! colspan="6" | Features
 |-
-! [[Higher-order logic]] !! [[Dependent type]]s !! [[de Bruijn criterion|Small kernel]] !! [[Proof automation]] !! [[Proof by reflection]] !! [[Code generation (compiler)|Code generation]]
+! [[Higher-order logic|उच्च-क्रम तर्क]] !! [[Dependent type|आश्रित प्रकार]] !! छोटा कर्नल !! [[Proof automation|प्रमाण स्वचालन]] !! [[Proof by reflection|प्रतिबिंब द्वारा प्रमाण]] !! [[Code generation (compiler)|कोड जनरेशन]]
 |-
-| [[ACL2]] || 8.3 || [[Matt Kaufmann]] and [[J Strother Moore]] ||  [[Common Lisp]]     || {{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}}
+| [[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}}
 |-
-| [[Agda (programming language)|Agda]] || 2.6.2
+| आग्डा || 2.6.2
-|| Ulf Norell, Nils Anders Danielsson, and Andreas Abel ([[Chalmers University of Technology|Chalmers]] and [[Gothenburg University|Gothenburg]]) ||[[Haskell (programming language)|Haskell]]|| {{yes}} || {{yes}} || {{yes}} || {{no}} || {{partial}} || {{n/a|Already executable}}
+|| उल्फ नॉरेल, निल्स एंडर्स डेनियलसन, और एंड्रियास एबेल (चेलमर्स और गोथेनबर्ग) ||[[हास्कल]]|| {{yes}} || {{yes}} || {{yes}} || {{no}} || {{partial}} || {{n/a|Already executable}}
 |-
 | [[Albatross (programming language)|Albatross]] || 0.4
-|| Helmut Brandl ||[[OCaml]]|| {{yes}} || {{no}} || {{yes}} || {{yes}} || {{unknown}} || {{not yet}} Implemented
+|| हेल्मुट ब्रैंडल ||[[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 || [[Microsoft Research]] and [[INRIA]] || [[F* (programming language)|F*]] || {{yes}} || {{yes}} || {{no}} || {{yes}} || {{yes}}<ref>Search for "proofs by reflection": {{ArXiv|1803.06547}}</ref> || {{yes}}
+| [[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 || John Harrison || [[OCaml]] || {{yes}} || {{no}} || {{yes}} || {{yes}} || {{no}} || {{no}}
+| [[HOL Light|एचओएल Light]] || repository || जॉन हैरिसन || [[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}}
+| [[HOL4|एचओएल4]] || Kananaskis-13 (or repo) || माइकल नॉरिश, कोनराड स्लिंड और अन्य || [[Standard ML|मानक एमएल]] || {{yes}} || {{no}} || {{yes}} || {{yes}} || {{no}} || {{yes}}
 |-
-| [[Idris (programming language)|Idris]] || 2 0.4.0. || Edwin Brady || [[Idris (programming language)|Idris]] || {{yes}} || {{yes}} || {{yes}} || {{unknown}} || {{partial}} || {{yes}}
+| [[Idris (programming language)|Idris]] || 2 0.4.0. || एडविन ब्रैडी || इदरिस || {{yes}} || {{yes}} || {{yes}} || {{unknown}} || {{partial}} || {{yes}}
 |-
-| [[Isabelle (proof assistant)|Isabelle]] || Isabelle2021 (February 2021) ||[[Larry Paulson]] ([[University of Cambridge|Cambridge]]), [[Tobias Nipkow]] ([[Technische Universität München|München]]) and [[Makarius Wenzel]] ||  [[Standard ML]], [[Scala (programming language)|Scala]]    || {{yes}} || {{no}}  || {{yes}} || {{yes}} || {{yes}} || {{yes}}
+| [[Isabelle (proof assistant)|Isabelle]] || Isabelle2021 (February 2021) ||लैरी पॉलसन (कैम्ब्रिज), टोबियास निप्को (मुन्चेन) और मैकरियस वेन्ज़ेल ||  मानक एमएल, स्काला    || {{yes}} || {{no}}  || {{yes}} || {{yes}} || {{yes}} || {{yes}}
 |-
 |[[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>
-|[[Leonardo de Moura]] [[Microsoft Research|(Microsoft Research]])
+|लियोनार्डो डी मौरा (माइक्रोसॉफ्ट रिसर्च)
-|[[C++]]
+|[[C++|सी++]]
 |{{yes}}
 |{{yes}}
@@ Line 44: / Line 44: @@
 |{{unknown}}
 |-
-| [[LEGO (proof assistant)|LEGO]] (not affiliated with [[Lego]]) || 1.3.1 || [[Randy Pollack]] ([[University of Edinburgh|Edinburgh]]) || [[Standard ML]] || {{yes}} || {{yes}} || {{yes}} || {{no}} || {{no}} || {{no}}
+| [[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]] || [[Free Pascal]] || {{partial}} || {{yes}} || {{no}} || {{no}} || {{no}} || {{no}}
+| [[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}}
 |-
-| [[Twelf]] || 1.7.1     || [[Frank Pfenning]] and [[Carsten Schürmann]] ||     [[Standard ML]]      || {{yes}} || {{yes}} || {{unknown}} || {{no}} || {{no}} || {{unknown}}
+| ट्वेल्फ || 1.7.1     || फ्रैंक पफेनिंग और कार्स्टन शूरमैन ||     [[Standard ML|मानक एमएल]]      || {{yes}} || {{yes}} || {{unknown}} || {{no}} || {{no}} || {{unknown}}
 |}
-* [[ACL2]] - बॉयर-मूर परंपरा में प्रोग्रामिंग भाषा, प्रथम-क्रम तार्किक सिद्धांत, और प्रमेय समर्थक (इंटरैक्टिव और स्वचालित मोड दोनों के साथ)।
+* [[ACL2|एसीएल 2]] - बॉयर-मूर परंपरा में प्रोग्रामिंग भाषा, प्रथम-क्रम तार्किक सिद्धांत है और प्रमेय समर्थक अर्ताथ इंटरैक्टिव और स्वचालित मोड दोनों के साथ संलग्न होकर कार्य करता हैं।
-* [[Coq]] – गणितीय अभिकथनों की अभिव्यक्ति की अनुमति देता है, यंत्रवत् रूप से इन अभिकथनों के प्रमाणों की जांच करता है, औपचारिक प्रमाणों को खोजने में मदद करता है, और इसके औपचारिक विनिर्देश के रचनात्मक प्रमाण से प्रमाणित कार्यक्रम निकालता है।
+* [[Coq|सीओक्यू]] – गणितीय अभिकथनों की अभिव्यक्ति की अनुमति देता है, यंत्रवत् रूप से इन अभिकथनों के प्रमाणों की जांच करता है, औपचारिक प्रमाणों को खोजने में मदद करता है, और इसके औपचारिक विनिर्देश के रचनात्मक प्रमाण से प्रमाणित कार्यक्रम निकालता है।
-* [[एचओएल प्रमेय समर्थक]] – उपकरणों का परिवार अंततः LCF थ्योरम प्रोवर से प्राप्त हुआ। इन प्रणालियों में तार्किक कोर उनकी प्रोग्रामिंग भाषा का पुस्तकालय है। प्रमेय भाषा के नए तत्वों का प्रतिनिधित्व करते हैं और केवल उन रणनीतियों के माध्यम से पेश किए जा सकते हैं जो तार्किक शुद्धता की गारंटी देते हैं। रणनीति संरचना उपयोगकर्ताओं को सिस्टम के साथ अपेक्षाकृत कम अंतःक्रियाओं के साथ महत्वपूर्ण प्रमाण प्रस्तुत करने की क्षमता देती है। परिवार के सदस्यों में शामिल हैं:
+* [[एचओएल प्रमेय समर्थक]] – उपकरणों का परिवार अंततः एलसीएफ थ्योरम प्रोवर से प्राप्त हुआ। इन प्रणालियों में तार्किक कोर उनकी प्रोग्रामिंग भाषा का पुस्तकालय है। प्रमेय भाषा के नए तत्वों का प्रतिनिधित्व करते हैं और केवल उन रणनीतियों के माध्यम से पेश किए जा सकते हैं जो तार्किक शुद्धता की गारंटी देते हैं। रणनीति संरचना उपयोगकर्ताओं को सिस्टम के साथ अपेक्षाकृत कम अंतःक्रियाओं के साथ महत्वपूर्ण प्रमाण प्रस्तुत करने की क्षमता देती है। परिवार के सदस्यों में सम्मिलित हैं:
-**[[HOL4]] – प्राथमिक वंशज , अभी भी सक्रिय विकास के अधीन है। [[मास्को एमएल]] और पॉली/एमएल दोनों के लिए समर्थन। बीएसडी-शैली का लाइसेंस है।
+**[[HOL4|एचओएल4]] – प्राथमिक वंशज , अभी भी सक्रिय विकास के अधीन है। [[मास्को एमएल]] और पॉली/एमएल दोनों के लिए समर्थन करते हैं तथा इसमें बीएसडी-शैली का लाइसेंस भी रहता है।
-** [[एचओएल लाइट]] - संपन्न न्यूनतम कांटा। [[ OCaml |OCaml]] आधारित।
+** [[एचओएल लाइट]] - यह मुख्य संपन्न न्यूनतम कांटा हैं। [[ OCaml |ओकैमल]] पर आधारित रहते हैं।
-**प्रूफपॉवर – मालिकाना हो गया, फिर ओपन सोर्स पर लौट आया। [[मानक एमएल]] के आधार पर।
+**प्रूफपॉवर – स्वयं का उत्तराधिकार होने के बाद फिर से ये ओपन सोर्स पर लौट आया है। जो [[मानक एमएल]] के आधार पर उपयोग किया जाता हैं।
-* 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>
+* आईएमपीएस, इंटरएक्टिव मैथमैटिकल प्रूफ सिस्टम हैं।<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 – इंटरएक्टिव थ्योरम प्रोवर भी सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित है, लेकिन तार्किक सिद्धांत और स्वतंत्र कार्यान्वयन के स्वतंत्र Q0 लॉजिक पर आधारित है।
+* [[प्रमेय साबित करने की प्रणाली|प्रमेय प्रमाणित करने की प्रणाली]] और ईटीपीएस – इंटरएक्टिव थ्योरम प्रोवर भी सामान्य रूप से टाइप किए गए लैम्ब्डा कैलकुलस पर आधारित है, लेकिन तार्किक सिद्धांत और स्वतंत्र कार्यान्वयन के स्वतंत्र क्यू0 लॉजिक पर आधारित है।
 == यूजर इंटरफेस ==
-प्रूफ असिस्टेंट के लिए लोकप्रिय फ्रंट-एंड [[Emacs]]- आधारित प्रूफ जनरल है, जिसे [[एडिनबर्ग विश्वविद्यालय]] में विकसित किया गया है।
+प्रूफ असिस्टेंट के लिए लोकप्रिय फ्रंट-एंड [[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>
+सीओक्यू में सीओक्यूआईडीई सम्मिलित है, जो ओकैमल/[[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|Computer-assisted proof}}
+*[[कंप्यूटर-सहायता प्रमाण]]
-* {{annotated link|Formal verification}}
+* [[औपचारिक सत्यापन]]
-* {{annotated link|Metamath}}
+* [[मेटामैथ]]
-* {{annotated link|QED manifesto}}
+* [[क्यूईडी घोषणापत्र]]
-* {{annotated link|Satisfiability modulo theories}}
+* [[संतुष्टि मॉड्यूल सिद्धांत]]
 == टिप्पणियाँ ==
@@ Line 100: / Line 100: @@
 * [https://theoremprover-museum.github.io/ Theorem Prover Museum]
 * [http://adam.chlipala.net/cpdt/html/Intro.html "Introduction"] in ''Certified Programming with Dependent Types''.
-* [http://video.ias.edu/univalent/appel Introduction to the Coq Proof Assistant] (with a general introduction to interactive theorem proving)
+* [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]
 * [https://github.com/johnyf/tool_lists/blob/master/verification_synthesis.md#theorem-provers A list of theorem proving tools]

Anonymous

Search

प्रमाण सहायक: Difference between revisions

Namespaces

More

Page actions

Revision as of 23:54, 7 March 2023

Contents

सिस्टम तुलना

यूजर इंटरफेस

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

प्रमाण सहायक: Difference between revisions

Revision as of 23:54, 7 March 2023

सिस्टम तुलना

यूजर इंटरफेस

यह भी देखें

टिप्पणियाँ

संदर्भ

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories