रॉबिन्सन की संकल्प प्रक्रिया की कमियां क्या थीं?
पॉलसन वगैरह। LCF से इसाबेल / HOL का कहना है:
प्रथम-क्रम तर्क के लिए संकल्प, सिद्धांत में पूर्ण लेकिन व्यवहार में अक्सर निराशाजनक।
मुझे लगता है कि पूर्ण का मतलब है कि वे प्रथम-क्रम तर्क में किसी भी सही सूत्र को सही कर सकते हैं। में स्वचालित तर्क की पुस्तिका मुझे लगता है:
संकल्प एक refutationally पूरा प्रमेय साबित विधि है: एक विरोधाभास (यानी, खाली खंड) खंड के किसी भी असंतोषजनक सेट से कटौती की जा सकती है।
विकिपीडिया से:
संतोषजनक फर्स्ट-ऑर्डर फॉर्मूले को असंतोषजनक साबित करने का प्रयास करने के परिणामस्वरूप एक गैर-गणना कम्प्यूटेशन हो सकता है
वह निराशाजनक क्यों है?
जवाब
जबकि "पूर्ण व्यवहार में निराशाजनक" निश्चित रूप से निश्चित नहीं है, "पूर्ण" के विपरीत (जिसका वास्तव में मतलब है "अंततः हर सच्चे सूत्र को साबित कर सकता है"), ऐसे उदाहरणों को खोजना बहुत आसान है जहां भोली संकल्प भी दूर से पर्याप्त नहीं है, अर्थात उदाहरण जो चाहिए साबित करना आसान है लेकिन कौन सा संकल्प बेहद धीमा है।
एक प्रसिद्ध उदाहरण कबूतर के छेद सिद्धांत के लिए एन्कोडिंग है$n$ प्रस्ताव तर्क में छेद (जो बयान है "$n+1$ कबूतर अंदर फिट नहीं हो सकते $n$डुप्लिकेट के बिना छेद)। इस बयान का कोई प्रमाण नहीं है, जिसमें केवल उप-घातीय में संकल्प का उपयोग किया गया है$n$।
भविष्यवाणी तर्क में चीजें और भी बदतर हैं, जहां बिना किसी तेज संकल्प प्रमाण के बयानों को खोजना बहुत आसान है।
ध्यान दें कि रिज़ॉल्यूशन को लागू करने के लिए रिज़ॉल्यूशन के किसी भी कार्यान्वयन को एक रणनीति लागू करनी चाहिए, जो पहले से ही एक बहुत ही कठिन समस्या है, और अनुसंधान का एक सक्रिय क्षेत्र है, क्योंकि प्रमेय साबित करने के लिए अधिकांश व्यावहारिक एल्गोरिदम भोले रिज़ॉल्यूशन की वृद्धि हैं, जैसे हाइपर-रिज़ॉल्यूशन ।