सुपरपोजिशन कैलकुलस: Difference between revisions

From Vigyanwiki
(Created page with "सुपरपोज़िशन कैलकुस समीकरण तर्क में स्वचालित प्रमेय साबित करने क...")
 
No edit summary
 
(4 intermediate revisions by 3 users not shown)
Line 1: Line 1:
सुपरपोज़िशन कैलकुस [[समीकरण तर्क]] में स्वचालित प्रमेय साबित करने के लिए एक [[औपचारिक प्रणाली]] है। यह 1990 के दशक की शुरुआत में विकसित किया गया था और ऑर्डर-आधारित समानता हैंडलिंग के साथ [[प्रथम-क्रम संकल्प]] से अवधारणाओं को जोड़ता है जैसा कि (अमोघ) Knuth-Bendix पूर्णता एल्गोरिदम | Knuth-Bendix पूर्णता के संदर्भ में विकसित किया गया था। इसे या तो संकल्प (समान तर्क के लिए) या असफल समापन (पूर्ण [[खंड]] तर्क के लिए) के सामान्यीकरण के रूप में देखा जा सकता है। अधिकांश प्रथम-क्रम तर्क की तरह | प्रथम-क्रम की गणना, सुपरपोज़िशन प्रथम-क्रम खंडों के एक सेट की ''असंतोषजनकता'' को दिखाने की कोशिश करता है, अर्थात यह खंडन द्वारा प्रमाण करता है। अध्यारोपण पूर्ण खंडन है - असीमित संसाधनों और एक ''निष्पक्ष'' व्युत्पत्ति रणनीति को देखते हुए, किसी भी असंतुष्ट खंड से एक विरोधाभास अंततः प्राप्त होगा।
सुपरपोज़िशन कैलकुस [[समीकरण तर्क]] में स्वचालित प्रमेय सिद्ध करने के लिए एक [[औपचारिक प्रणाली]] है। यह 1990 के दशक की प्रारंभिक में विकसित किया गया था और ऑर्डर-आधारित समानता हैंडलिंग के साथ [[प्रथम-क्रम संकल्प]] से अवधारणाओं को जोड़ता है जैसा कि (अमोघ) नुथ-बेंडिक्स पूर्णता कलन विधि| इसे या तो संकल्प के सामान्यीकरण के रूप में देखा जा सकता है (समान तर्क के लिए) या अचूक समापन (पूर्ण खंड तर्क के लिए)अधिकांश प्रथम-क्रम की गणना की तरह, सुपरपोज़िशन प्रथम-क्रम खंडों के एक सेट की ''असंतोषजनकता'' को दिखाने की कोशिश करता है, अर्थात यह खंडन के माध्यम से  प्रमाण करता है। अध्यारोपण पूर्ण खंडन है - असीमित संसाधनों और एक ''निष्पक्ष'' व्युत्पत्ति रणनीति को देखते हुए, किसी भी असंतुष्ट खंड से एक विरोधाभास अंततः प्राप्त होगा।


{{As of|2007}}, प्रथम-क्रम तर्क के लिए अधिकांश (अत्याधुनिक) स्वचालित प्रमेय सिद्ध सुपरपोजिशन पर आधारित हैं (उदाहरण के लिए ई समीकरण प्रमेय कहावत), हालांकि केवल कुछ ही शुद्ध कलन को लागू करते हैं।
{{As of|2007}}, प्रथम-क्रम तर्क के लिए अधिकांश (अत्याधुनिक) स्वचालित प्रमेय सिद्ध सुपरपोजिशन पर आधारित हैं (उदाहरण के लिए ई समीकरण प्रमेय कहावत), चूंकि एकमात्र कुछ ही शुद्ध कलन को लागू करते हैं।


== कार्यान्वयन ==
== कार्यान्वयन ==
Line 8: Line 8:
* SPASS प्रमेय कहावत
* SPASS प्रमेय कहावत
* वैम्पायर प्रमेय प्रवर्तक
* वैम्पायर प्रमेय प्रवर्तक
* Waldmeister प्रमेय समर्थक [https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/waldmeister/ (आधिकारिक वेब पेज)]
* वाल्डमिस्टर प्रमेय समर्थक [https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/waldmeister/ (आधिकारिक वेब पेज)]


== संदर्भ ==
== संदर्भ ==
Line 14: Line 14:
* ''[http://pubman.mpdl.mpg.de/pubman/item/escidoc:1834970/component/escidoc:1857487/MPI-I-91-208.pdf Rewrite-Based Equational Theorem Proving with Selection and Simplification]'', Leo Bachmair and [[Harald Ganzinger]], [[Journal of Logic and Computation]] 3(4), 1994.
* ''[http://pubman.mpdl.mpg.de/pubman/item/escidoc:1834970/component/escidoc:1857487/MPI-I-91-208.pdf Rewrite-Based Equational Theorem Proving with Selection and Simplification]'', Leo Bachmair and [[Harald Ganzinger]], [[Journal of Logic and Computation]] 3(4), 1994.
* ''Paramodulation-Based Theorem Proving'', Robert Nieuwenhuis and Alberto Rubio, [[Handbook of Automated Reasoning]] I(7), [[Elsevier]] Science and [[MIT Press]], 2001.
* ''Paramodulation-Based Theorem Proving'', Robert Nieuwenhuis and Alberto Rubio, [[Handbook of Automated Reasoning]] I(7), [[Elsevier]] Science and [[MIT Press]], 2001.
[[Category: गणितीय तर्क]] [[Category: तार्किक गणना]]
 
{{mathlogic-stub}}
{{mathlogic-stub}}


 
[[Category:All articles containing potentially dated statements]]
 
[[Category:All stub articles]]
[[Category: Machine Translated Page]]
[[Category:Articles containing potentially dated statements from 2007]]
[[Category:Created On 18/05/2023]]
[[Category:Created On 18/05/2023]]
[[Category:Machine Translated Page]]
[[Category:Mathematical logic stubs]]
[[Category:गणितीय तर्क]]
[[Category:तार्किक गणना]]

Latest revision as of 18:38, 15 June 2023

सुपरपोज़िशन कैलकुस समीकरण तर्क में स्वचालित प्रमेय सिद्ध करने के लिए एक औपचारिक प्रणाली है। यह 1990 के दशक की प्रारंभिक में विकसित किया गया था और ऑर्डर-आधारित समानता हैंडलिंग के साथ प्रथम-क्रम संकल्प से अवधारणाओं को जोड़ता है जैसा कि (अमोघ) नुथ-बेंडिक्स पूर्णता कलन विधि| इसे या तो संकल्प के सामान्यीकरण के रूप में देखा जा सकता है (समान तर्क के लिए) या अचूक समापन (पूर्ण खंड तर्क के लिए)। अधिकांश प्रथम-क्रम की गणना की तरह, सुपरपोज़िशन प्रथम-क्रम खंडों के एक सेट की असंतोषजनकता को दिखाने की कोशिश करता है, अर्थात यह खंडन के माध्यम से प्रमाण करता है। अध्यारोपण पूर्ण खंडन है - असीमित संसाधनों और एक निष्पक्ष व्युत्पत्ति रणनीति को देखते हुए, किसी भी असंतुष्ट खंड से एक विरोधाभास अंततः प्राप्त होगा।

As of 2007, प्रथम-क्रम तर्क के लिए अधिकांश (अत्याधुनिक) स्वचालित प्रमेय सिद्ध सुपरपोजिशन पर आधारित हैं (उदाहरण के लिए ई समीकरण प्रमेय कहावत), चूंकि एकमात्र कुछ ही शुद्ध कलन को लागू करते हैं।

कार्यान्वयन

  • ई समीकरण प्रमेय कहावत
  • SPASS प्रमेय कहावत
  • वैम्पायर प्रमेय प्रवर्तक
  • वाल्डमिस्टर प्रमेय समर्थक (आधिकारिक वेब पेज)

संदर्भ