दो-चर तर्क

मैथमेटिकल लॉजिक और कंप्यूटर विज्ञान में, टू वेरिएबल लॉजिक फर्स्ट आर्डर लॉजिक का फ्रेगमेंट है जहां फोर्मुला (लॉजिक ) केवल दो अलग-अलग वेरिएबल (लॉजिक ) का उपयोग करके लिखा जा सकता है। इस फ्रेगमेंट का अध्ययन सामान्यतः फंक्शन सिंबल के बिना किया जाता है।

डिसाइडेबल

टू वेरिएबल लॉजिक के बारे में कुछ महत्वपूर्ण समस्याएं जैसे सेटीसफियाबिलिटी(लॉजिक ) और फाईनाईट सेटीसफियाबिलिटी (लॉजिक ), डिसाइडेबल (कंप्यूटर विज्ञान) हैं। यह परिणाम टू वेरिएबल लॉजिक के टुकड़ों की डिसाइडेबल के बारे में परिणामों को सामान्यीकृत करता है, जैसे कि कुछ डिस्क्रिप्शन लॉजिक; चूँकि, टू वेरिएबल लॉजिक के कुछ फ्रेगमेंट उनकी सेटीसफियाबिलिटी समस्याओं के लिए बहुत कम कम्प्यूटेशनल समष्टियता सिद्धांत का प्रयोग करते हैं।

इसके विपरीत, फंक्शन सिंबल के बिना फर्स्ट आर्डर लॉजिक के तीन-वेरिएबल फ्रेगमेंट के लिए सेटीसफियाबिलिटी अनडिसाइडेबल है।

काउंटिंग क्कंटीफायर

फंक्शन सिंबल वाले फर्स्ट आर्डर लॉजिक के टू वेरिएबल फ्रेगमेंट को काउंटिंग क्कंटीफायर को जोड़ने के साथ भी निर्णय लेने योग्य माना जाता है, और इस प्रकार यूनिकनेस क्कंटीफिकैसन यह एक अधिक शक्तिशाली परिणाम है, क्योंकि उच्च संख्यात्मक मानों के लिए गणना परिमाणक उस लॉजिक में व्यक्त नहीं किए जा सकते हैं।

गणना परिमाणक वास्तव में परिमित-परिवर्तनीय लॉजिक ों की अभिव्यक्ति में सुधार करते हैं क्योंकि वे यह कहने की अनुमति देते हैं कि $n$ निकटतम के साथ एक नोड है, अर्थात् $\Phi =\exists x\exists ^{\geq n}yE(x,y)$ परिमाणकों की गिनती के बिना समान फोर्मुला के लिए $n+1$ वेरिएबल की आवश्यकता होती है।

वीस्फ़ीलर-लेमन एल्गोरिथम से कनेक्शन

टू वेरिएबल लॉजिक और वीस्फ़ीलर-लेमन (या कलर रेफिनमेंट ) एल्गोरिदम के बीच एक शक्तिशाली संबंध है। दो ग्राफ़ दिए गए हैं, तो किन्हीं दो नोड्स में कलर रेफिनमेंट में एक ही स्थिर कलर होता है यदि और केवल यदि उनके पास समान $C^{2}$ प्रकार है, अर्थात् वे गिनती के साथ टू वेरिएबल लॉजिक में समान सूत्रों को संतुष्ट करते हैं।