Title of the talk: On Merge Resolution proof system for Quantified Boolean Formulas

Date & Time: 13 November 2025 at 12 noon (ONLINE)

सार: हम उन प्रमाणों का अध्ययन करते हैं कि n-चर डायोफैंटाइन रैखिक समीकरणों (या बूलियन सूत्रों) की एक प्रणाली का कोई {0,1} हल नहीं होता है। जबकि एक तुच्छ प्रमाण सभी 2^n संभावित असाइनमेंट की जाँच करता है, कम्प्यूटेशनल जटिलता सिद्धांत में एक प्रमुख खुला प्रश्न यह पूछता है कि क्या छोटे (अर्थात n में लंबाई वाले बहुपद) प्रमाण मौजूद हैं। एक प्रारंभिक चरण के रूप में, एक विशिष्ट प्रमाण प्रारूप तय किया जाता है और पूछा जाता है कि क्या सभी असंतोषजनक प्रणालियों में उस प्रमाण प्रारूप में छोटे प्रमाण होते हैं।

हम उन प्रणालियों का अध्ययन करते हैं जिनमें कुछ चर सार्वभौमिक रूप से परिमाणित होते हैं और मर्ज रिज़ॉल्यूशन नामक एक विशिष्ट प्रमाण प्रारूप का अध्ययन करते हैं। हम दिखाते हैं कि ऐसी प्रणालियाँ हैं जिनके लिए मर्ज रिज़ॉल्यूशन में लंबे (अर्थात घातांकीय आकार) प्रमाणों की आवश्यकता होती है।

वक्ता के बारे में: डॉ. गौरव सूद आईआईटी मंडी (कंप्यूटिंग और इलेक्ट्रिकल इंजीनियरिंग स्कूल) में सहायक प्रोफेसर हैं। उन्होंने 2023 में चेन्नई के गणितीय विज्ञान संस्थान से पीएचडी और कंप्यूटर विज्ञान और इंजीनियरिंग में एम.टेक की उपाधि प्राप्त की। उन्होंने 2013 में राष्ट्रीय प्रौद्योगिकी संस्थान कालीकट से एम.डी. की उपाधि प्राप्त की। इससे पहले वे टेक्नियन, इज़राइल (कंप्यूटर विज्ञान विभाग) में पोस्टडॉक्टरल फेलो थे।