सुपरपोजिशन कैलकुलस

From Vigyanwiki

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

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

कार्यान्वयन

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

संदर्भ