विभेदन विधि

प्रस्तावात्मक तर्क के अर्थविज्ञान वाले पाठ ने दिखाया कि वैधता और संतोषणीयता सत्यता सारणी द्वारा निर्णेय हैं, ऐसी लागत पर जो हर चर के साथ दुगुनी हो जाती है, और ऐसी विधियों की घोषणा की जिनमें उसे पूरा खंगालना आवश्यक न हो। शब्दार्थीय परिणाम और शब्दार्थीय तुल्यता वाले पाठ ने प्रत्येक परिणाम को एक असंतोषणीयता में बदल दिया: $\Gamma \models \varphi$ यदि और केवल यदि $\Gamma \cup \{\neg\varphi\}$ असंतोषणीय है। प्रसामान्य रूपों और उनकी कलन-विधि वाले पाठों ने प्रत्येक सूत्र को एक संयोजक रूप दिया, जिसकी वैधता एक दृष्टि में दिख जाती है, पर जिसकी संतोषणीयता नहीं दिखती। यदि ऐसा है, तो एक ऐसी प्रक्रिया की कमी है जो उपवाक्यों के किसी संयोजन की असंतोषणीयता का निर्णय स्वयं उपवाक्यों पर काम करते हुए करे। वह प्रक्रिया विभेदन है, जिसे जॉन एलन रॉबिन्सन ने 1965 में मार्टिन डेविस और हिलेरी पटनम (1960) के विचारों के आधार पर प्रस्तावित किया; यह उन प्रोग्रामों का केंद्र है जो आज दसियों लाख चरों वाले सूत्रों की संतोषणीयता का निर्णय करते हैं। निगमन की इकाई की प्रणाली से भिन्न, जिसके अर्थविज्ञान के साथ संबंधों का अध्ययन सुदृढ़ता और पूर्णता और संहतता प्रमेय वाले पाठ करते हैं, विभेदन निष्कर्षों का निगमन नहीं करता: वह समुच्चयों का खंडन करता है। यह पाठ सिद्ध करता है कि वह यह काम सुदृढ़ और पूर्ण ढंग से करता है।

पिछले पाठों की तरह, $p$, $q$, $r$, $s$ और $t$ चरों $v_1$ से $v_5$ तक के नाम हैं; बिना पादांक का अक्षर $v$, और $w$ भी, मान-नियतनों को सूचित करते हैं; और $V(\varphi)$, $\varphi$ के चरों का समुच्चय है।

उपवाक्य और उपवाक्यों के समुच्चय

प्रसामान्य रूपों वाले पाठ से याद करें कि लिटरल एक चर या किसी चर का निषेध है, और किसी लिटरल $\ell$ का विपरीत, जिसे $\ell^{*}$ लिखा जाता है, उसी चर का दूसरे चिह्न वाला लिटरल है; दो विपरीत लिटरल एक पूरक युग्म बनाते हैं। लिटरल के निषेध की प्रमेयिका से, $v(\ell^{*}) = 1 - v(\ell)$, प्रत्येक मान-नियतन $v$ के लिए। वहाँ उपवाक्य लिटरलों का एक वियोजन था; यहाँ क्रम और पुनरावृत्तियों को, जो मान नहीं बदलतीं, भूल जाना और केवल समुच्चय को रखना सुविधाजनक है।

उपवाक्य लिटरलों का एक परिमित समुच्चय है। बिना लिटरलों वाले उपवाक्य को रिक्त उपवाक्य कहते हैं और उसे $\Box$ लिखा जाता है। एक मान-नियतन $v$ किसी उपवाक्य $C$ को संतुष्ट करता है, और लिखा जाता है $v \models C$, यदि $C$ के किसी लिटरल का मान $1$ हो ($v$ के अंतर्गत); अन्यथा $v$ उसे खंडित करता है। केवल एक लिटरल वाले उपवाक्य को एकल उपवाक्य कहते हैं। किसी उपवाक्य के चर समुच्चय $V(C)$ बनाते हैं; उपवाक्यों के किसी समुच्चय $S$ के चर समुच्चय $V(S)$ बनाते हैं, जो पिछले समुच्चयों का सम्मिलन है। एक मान-नियतन उपवाक्यों के किसी समुच्चय $S$ को संतुष्ट करता है, $v \models S$, यदि वह उसके प्रत्येक उपवाक्य को संतुष्ट करता है; $S$ संतोषणीय है यदि कोई मान-नियतन उसे संतुष्ट करता है, और अन्यथा असंतोषणीय। अंत में, यदि $S$ उपवाक्यों का एक समुच्चय है और $C$ एक उपवाक्य, तो $S \models C$ का अर्थ है कि $S$ को संतुष्ट करने वाला प्रत्येक मान-नियतन $C$ को संतुष्ट करता है।

परिभाषा से दो चरम स्थितियाँ निकलती हैं, और उन्हें स्पष्ट कर लेना उचित है। रिक्त उपवाक्य में कोई लिटरल नहीं है; अतः उसके किसी लिटरल का मान $1$ नहीं है, और कोई मान-नियतन उसे संतुष्ट नहीं करता: $\Box$ असंतोषणीय है, और उसे समाविष्ट करने वाला प्रत्येक समुच्चय भी। इसके विपरीत, उपवाक्यों के रिक्त समुच्चय में संतुष्ट करने के लिए कोई उपवाक्य नहीं है, और प्रत्येक मान-नियतन उसे संतुष्ट करता है। इन्हें एक-दूसरे से भ्रमित नहीं करना चाहिए: $\{\Box\}$ असंतोषणीय है और $\emptyset$ को सभी मान-नियतन संतुष्ट करते हैं।

जिस उपवाक्य में कोई पूरक युग्म हो उसे पुनरुक्तिपरक कहते हैं: वह कोई प्रतिबंध नहीं लगाता, और उसे किसी भी समुच्चय से उसके मॉडल बदले बिना हटाया जा सकता है। उपवाक्यों को समुच्चयों के रूप में लिखना संकेतन की सनक नहीं है। यदि $(p \vee q)$ और $(p \vee \neg q)$ से $p$ प्राप्त करना हो, तो वियोजन $(p \vee p)$ देता है, जो $p$ के तुल्य है पर वही सूत्र नहीं है; समुच्चयों के साथ $\{p\} \cup \{p\} = \{p\}$, और दोहराए गए लिटरलों का विलय अपने-आप हो जाता है।