सुपरपोजिशन कैलकुलस: Difference between revisions
(Created page with "सुपरपोज़िशन कैलकुस समीकरण तर्क में स्वचालित प्रमेय साबित करने क...") |
No edit summary |
||
| Line 1: | Line 1: | ||
सुपरपोज़िशन कैलकुस [[समीकरण तर्क]] में स्वचालित प्रमेय | सुपरपोज़िशन कैलकुस [[समीकरण तर्क]] में स्वचालित प्रमेय सिद्ध करने के लिए एक [[औपचारिक प्रणाली]] है। यह 1990 के दशक की शुरुआत में विकसित किया गया था और ऑर्डर-आधारित समानता हैंडलिंग के साथ [[प्रथम-क्रम संकल्प]] से अवधारणाओं को जोड़ता है जैसा कि (अमोघ) नुथ-बेंडिक्स पूर्णता कलन विधि| इसे या तो संकल्प के सामान्यीकरण के रूप में देखा जा सकता है (समान तर्क के लिए) या अचूक समापन (पूर्ण खंड तर्क के लिए)। अधिकांश प्रथम-क्रम की गणना की तरह, सुपरपोज़िशन प्रथम-क्रम खंडों के एक सेट की ''असंतोषजनकता'' को दिखाने की कोशिश करता है, अर्थात यह खंडन द्वारा प्रमाण करता है। अध्यारोपण पूर्ण खंडन है - असीमित संसाधनों और एक ''निष्पक्ष'' व्युत्पत्ति रणनीति को देखते हुए, किसी भी असंतुष्ट खंड से एक विरोधाभास अंततः प्राप्त होगा। | ||
{{As of|2007}}, प्रथम-क्रम तर्क के लिए अधिकांश (अत्याधुनिक) स्वचालित प्रमेय सिद्ध सुपरपोजिशन पर आधारित हैं (उदाहरण के लिए ई समीकरण प्रमेय कहावत), हालांकि केवल कुछ ही शुद्ध कलन को लागू करते हैं। | {{As of|2007}}, प्रथम-क्रम तर्क के लिए अधिकांश (अत्याधुनिक) स्वचालित प्रमेय सिद्ध सुपरपोजिशन पर आधारित हैं (उदाहरण के लिए ई समीकरण प्रमेय कहावत), हालांकि केवल कुछ ही शुद्ध कलन को लागू करते हैं। | ||
| Line 8: | Line 8: | ||
* SPASS प्रमेय कहावत | * SPASS प्रमेय कहावत | ||
* वैम्पायर प्रमेय प्रवर्तक | * वैम्पायर प्रमेय प्रवर्तक | ||
* | * वाल्डमिस्टर प्रमेय समर्थक [https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/waldmeister/ (आधिकारिक वेब पेज)] | ||
== संदर्भ == | == संदर्भ == | ||
Revision as of 02:37, 21 May 2023
सुपरपोज़िशन कैलकुस समीकरण तर्क में स्वचालित प्रमेय सिद्ध करने के लिए एक औपचारिक प्रणाली है। यह 1990 के दशक की शुरुआत में विकसित किया गया था और ऑर्डर-आधारित समानता हैंडलिंग के साथ प्रथम-क्रम संकल्प से अवधारणाओं को जोड़ता है जैसा कि (अमोघ) नुथ-बेंडिक्स पूर्णता कलन विधि| इसे या तो संकल्प के सामान्यीकरण के रूप में देखा जा सकता है (समान तर्क के लिए) या अचूक समापन (पूर्ण खंड तर्क के लिए)। अधिकांश प्रथम-क्रम की गणना की तरह, सुपरपोज़िशन प्रथम-क्रम खंडों के एक सेट की असंतोषजनकता को दिखाने की कोशिश करता है, अर्थात यह खंडन द्वारा प्रमाण करता है। अध्यारोपण पूर्ण खंडन है - असीमित संसाधनों और एक निष्पक्ष व्युत्पत्ति रणनीति को देखते हुए, किसी भी असंतुष्ट खंड से एक विरोधाभास अंततः प्राप्त होगा।
As of 2007[update], प्रथम-क्रम तर्क के लिए अधिकांश (अत्याधुनिक) स्वचालित प्रमेय सिद्ध सुपरपोजिशन पर आधारित हैं (उदाहरण के लिए ई समीकरण प्रमेय कहावत), हालांकि केवल कुछ ही शुद्ध कलन को लागू करते हैं।
कार्यान्वयन
- ई समीकरण प्रमेय कहावत
- SPASS प्रमेय कहावत
- वैम्पायर प्रमेय प्रवर्तक
- वाल्डमिस्टर प्रमेय समर्थक (आधिकारिक वेब पेज)
संदर्भ
- 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.
 | This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |
