सुपरपोजिशन कैलकुलस
सुपरपोज़िशन कैलकुस समीकरण तर्क में स्वचालित प्रमेय साबित करने के लिए एक औपचारिक प्रणाली है। यह 1990 के दशक की शुरुआत में विकसित किया गया था और ऑर्डर-आधारित समानता हैंडलिंग के साथ प्रथम-क्रम संकल्प से अवधारणाओं को जोड़ता है जैसा कि (अमोघ) Knuth-Bendix पूर्णता एल्गोरिदम | Knuth-Bendix पूर्णता के संदर्भ में विकसित किया गया था। इसे या तो संकल्प (समान तर्क के लिए) या असफल समापन (पूर्ण खंड तर्क के लिए) के सामान्यीकरण के रूप में देखा जा सकता है। अधिकांश प्रथम-क्रम तर्क की तरह | प्रथम-क्रम की गणना, सुपरपोज़िशन प्रथम-क्रम खंडों के एक सेट की असंतोषजनकता को दिखाने की कोशिश करता है, अर्थात यह खंडन द्वारा प्रमाण करता है। अध्यारोपण पूर्ण खंडन है - असीमित संसाधनों और एक निष्पक्ष व्युत्पत्ति रणनीति को देखते हुए, किसी भी असंतुष्ट खंड से एक विरोधाभास अंततः प्राप्त होगा।
As of 2007[update], प्रथम-क्रम तर्क के लिए अधिकांश (अत्याधुनिक) स्वचालित प्रमेय सिद्ध सुपरपोजिशन पर आधारित हैं (उदाहरण के लिए ई समीकरण प्रमेय कहावत), हालांकि केवल कुछ ही शुद्ध कलन को लागू करते हैं।
कार्यान्वयन
- ई समीकरण प्रमेय कहावत
- SPASS प्रमेय कहावत
- वैम्पायर प्रमेय प्रवर्तक
- Waldmeister प्रमेय समर्थक (आधिकारिक वेब पेज)
संदर्भ
- 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. |
