कंप्यूटर विज्ञान में तर्क: Difference between revisions
From Vigyanwiki
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
{{for|[[शैक्षणिक सम्मेलन]] एलआईसी|कंप्यूटर विज्ञान में तर्क पर संगोष्ठी}} | {{for|[[शैक्षणिक सम्मेलन]] एलआईसी|कंप्यूटर विज्ञान में तर्क पर संगोष्ठी}} | ||
{{short description|Academic discipline}} | {{short description|Academic discipline}} | ||
[[File:Logic Gates.svg|thumbnail|right|कंप्यूटर [[ तर्क द्वार ]] का आरेखीय प्रतिनिधित्व]][[कंप्यूटर विज्ञान]] में [[तर्क]] और कंप्यूटर विज्ञान के क्षेत्र के | [[File:Logic Gates.svg|thumbnail|right|कंप्यूटर [[ तर्क द्वार ]] का आरेखीय प्रतिनिधित्व]][[कंप्यूटर विज्ञान]] में [[तर्क]] और कंप्यूटर विज्ञान के क्षेत्र के मध्य ओवरलैप को कवर करता है। विषय को अनिवार्य रूप से तीन मुख्य क्षेत्रों में विभाजित किया जा सकता है: | ||
* सैद्धांतिक नींव और | * सैद्धांतिक नींव और विश्लेषण। | ||
* तर्कशास्त्रियों की सहायता के लिए कंप्यूटर प्रौद्योगिकी का | * तर्कशास्त्रियों की सहायता के लिए कंप्यूटर प्रौद्योगिकी का उपयोग। | ||
* कंप्यूटर अनुप्रयोगों के लिए तर्क से अवधारणाओं का | * कंप्यूटर अनुप्रयोगों के लिए तर्क से अवधारणाओं का उपयोग। | ||
== सैद्धांतिक नींव और विश्लेषण == | == सैद्धांतिक नींव और विश्लेषण == | ||
तर्क कंप्यूटर विज्ञान में मौलिक भूमिका निभाता है। तर्क के कुछ प्रमुख क्षेत्र जो विशेष रूप से महत्वपूर्ण हैं, संगणना सिद्धांत (पूर्व में पुनरावर्तन सिद्धांत कहा जाता है), [[मॉडल तर्क]] और [[श्रेणी सिद्धांत]] हैं। अभिकलन का सिद्धांत | तर्क कंप्यूटर विज्ञान में मौलिक भूमिका निभाता है। तर्क के कुछ प्रमुख क्षेत्र जो विशेष रूप से महत्वपूर्ण हैं, संगणना सिद्धांत (पूर्व में पुनरावर्तन सिद्धांत कहा जाता है), [[मॉडल तर्क]] और [[श्रेणी सिद्धांत]] हैं। अभिकलन का सिद्धांत [[अलोंजो चर्च]] और [[एलन ट्यूरिंग]] जैसे तर्कशास्त्रियों और गणितज्ञों द्वारा परिभाषित अवधारणाओं पर आधारित है।<ref>{{cite book|last=Lewis|first=Harry R.|url=https://archive.org/details/elementsoftheory00lewi|title=संगणना के सिद्धांत के तत्व|publisher=[[Prentice Hall]]|year=1981|author-link=Harry R. Lewis}}</ref><ref>{{cite book|last=Davis|first=Martin|title=यूनिवर्सल ट्यूरिंग मशीन|publisher=Springer Verlag|chapter-url=https://books.google.com/books?id=YafIDVd1Z68C&pg=PA290|editor=Rolf Herken|access-date=26 December 2013|chapter=Influences of Mathematical Logic on Computer Science|date=11 May 1995|isbn=9783211826379|author-link=Martin Davis (mathematician)}}</ref> चर्च ने सर्वप्रथम लैम्ब्डा-निश्चितता की अपनी धारणा का उपयोग करके एल्गोरिथम रूप से अघुलनशील समस्याओं का अस्तित्व दिखाया है। ट्यूरिंग ने प्रथम सम्मोहक विश्लेषण दिया जिसे यांत्रिक प्रक्रिया कहा जा सकता है और कर्ट गोडेल ने जोर देकर कहा कि उन्होंने ट्यूरिंग के विश्लेषण को सही पाया है।<ref>{{cite book|last=Kennedy|first=Juliette|title=गोडेल की व्याख्या करना|publisher=Cambridge University Press|url=https://books.google.com/books?id=ulw3BAAAQBAJ&q=Godel+convinced+by+Turing%27s+analysis&pg=PA118|access-date= 17 August 2015|isbn=9781107002661|date=2014-08-21}}</ref> इसके अतिरिक्त तर्क और कंप्यूटर विज्ञान के मध्य सैद्धांतिक ओवरलैप के कुछ अन्य प्रमुख क्षेत्र हैं: | ||
इसके | |||
* गोडेल की अपूर्णता प्रमेय यह साबित करती है कि अंकगणित की विशेषता के लिए पर्याप्त शक्तिशाली किसी भी तार्किक प्रणाली में ऐसे कथन होंगे जो उस प्रणाली के भीतर न तो सिद्ध किए जा सकते हैं और न ही अस्वीकृत। सॉफ्टवेयर की पूर्णता और शुद्धता को साबित करने की व्यवहार्यता से संबंधित सैद्धांतिक मुद्दों पर इसका सीधा अनुप्रयोग है।<ref>{{cite book|last=Hofstadter|first=Douglas R.|title=Gödel, Escher, Bach: An Eternal Golden Braid|publisher=Basic Books|isbn=978-0465026562|author-link=Douglas Hofstadter|url=https://archive.org/details/gdelescherbachet00hofs|date=1999-02-05}}</ref> *फ़्रेम की समस्या बुनियादी समस्या है जिसे आर्टिफिशियल इंटेलिजेंस एजेंट के लक्ष्यों और स्थिति का प्रतिनिधित्व करने के लिए [[पहले क्रम का तर्क]] का उपयोग करते समय दूर किया जाना चाहिए।<ref>{{cite journal|last=McCarthy|first=John|author2=P.J. Hayes |title=कृत्रिम बुद्धि के दृष्टिकोण से कुछ दार्शनिक समस्याएं|journal=Machine Intelligence|year=1969|volume=4|pages=463–502|author-link1=John McCarthy (computer scientist)|url=http://www-formal.stanford.edu/jmc/mcchay69.pdf}}</ref> | * गोडेल की अपूर्णता प्रमेय यह साबित करती है कि अंकगणित की विशेषता के लिए पर्याप्त शक्तिशाली किसी भी तार्किक प्रणाली में ऐसे कथन होंगे जो उस प्रणाली के भीतर न तो सिद्ध किए जा सकते हैं और न ही अस्वीकृत। सॉफ्टवेयर की पूर्णता और शुद्धता को साबित करने की व्यवहार्यता से संबंधित सैद्धांतिक मुद्दों पर इसका सीधा अनुप्रयोग है।<ref>{{cite book|last=Hofstadter|first=Douglas R.|title=Gödel, Escher, Bach: An Eternal Golden Braid|publisher=Basic Books|isbn=978-0465026562|author-link=Douglas Hofstadter|url=https://archive.org/details/gdelescherbachet00hofs|date=1999-02-05}}</ref> *फ़्रेम की समस्या बुनियादी समस्या है जिसे आर्टिफिशियल इंटेलिजेंस एजेंट के लक्ष्यों और स्थिति का प्रतिनिधित्व करने के लिए [[पहले क्रम का तर्क]] का उपयोग करते समय दूर किया जाना चाहिए।<ref>{{cite journal|last=McCarthy|first=John|author2=P.J. Hayes |title=कृत्रिम बुद्धि के दृष्टिकोण से कुछ दार्शनिक समस्याएं|journal=Machine Intelligence|year=1969|volume=4|pages=463–502|author-link1=John McCarthy (computer scientist)|url=http://www-formal.stanford.edu/jmc/mcchay69.pdf}}</ref> | ||
<!-- *[[Category theory]] is the formal analysis and transformation of [[Graph theory|directed graphs]], an area with some applications in computer science, most notably programming languages and compilers.<ref>{{cite journal|last=DeLoach|first=Scott|author2=Thomas Hartrum |title=A Theory Based Representation for Object-Oriented Domain Models|journal=IEEE Transactions on Software Engineering|date=June 2000|volume=25|issue=6|doi=10.1109/32.852740|pages=500–517}}</ref> --> | <!-- *[[Category theory]] is the formal analysis and transformation of [[Graph theory|directed graphs]], an area with some applications in computer science, most notably programming languages and compilers.<ref>{{cite journal|last=DeLoach|first=Scott|author2=Thomas Hartrum |title=A Theory Based Representation for Object-Oriented Domain Models|journal=IEEE Transactions on Software Engineering|date=June 2000|volume=25|issue=6|doi=10.1109/32.852740|pages=500–517}}</ref> --> | ||
*करी-हावर्ड पत्राचार तार्किक प्रणालियों और सॉफ्टवेयर के | *करी-हावर्ड पत्राचार तार्किक प्रणालियों और सॉफ्टवेयर के मध्य संबंध है। इस सिद्धांत ने प्रमाणों और कार्यक्रमों के मध्य सटीक पत्राचार स्थापित किया। विशेष रूप से यह दिखाया गया है कि सामान्य रूप से टाइप किए गए लैम्ब्डा-कैलकुलस में शब्द अंतर्ज्ञानवादी प्रस्तावपरक तर्क के प्रमाण के अनुरूप हैं। | ||
*श्रेणी सिद्धांत गणित के दृष्टिकोण का प्रतिनिधित्व करता है जो संरचनाओं के | *श्रेणी सिद्धांत गणित के दृष्टिकोण का प्रतिनिधित्व करता है जो संरचनाओं के मध्यसंबंधों पर जोर देता है। यह कंप्यूटर विज्ञान के कई पहलुओं से घनिष्ठ रूप से जुड़ा हुआ है: प्रोग्रामिंग भाषाओं के लिए टाइप सिस्टम, ट्रांज़िशन सिस्टम का सिद्धांत, प्रोग्रामिंग भाषाओं के मॉडल और प्रोग्रामिंग भाषा शब्दार्थ का सिद्धांत।<ref>{{cite book|first=Michael|last=Barr|title=कम्प्यूटिंग विज्ञान के लिए श्रेणी सिद्धांत|year=1998|author2=Charles Wells|url=https://www.math.mcgill.ca/barr/papers/ctcs.pdf|publisher=[[Centre de Recherches Mathématiques]]}}</ref> | ||
== तर्कशास्त्रियों की सहायता के लिए कंप्यूटर == | == तर्कशास्त्रियों की सहायता के लिए कंप्यूटर == | ||
[[ कृत्रिम होशियारी ]] शब्द का उपयोग करने वाले पहले अनुप्रयोगों में से 1956 में [[एलन नेवेल]], जे.सी. शॉ और हर्बर्ट ए. साइमन द्वारा विकसित लॉजिक थिओरिस्ट सिस्टम था। उन निष्कर्षों (अतिरिक्त कथनों) को निकालें जो तर्क के नियमों द्वारा सत्य होने चाहिए। उदाहरण के लिए, यदि तार्किक प्रणाली दी गई है जो बताती है कि सभी मनुष्य नश्वर हैं और सुकरात मानव हैं तो मान्य निष्कर्ष यह है कि सुकरात नश्वर है। बेशक यह तुच्छ उदाहरण है। वास्तविक तार्किक प्रणालियों में कथन असंख्य और जटिल हो सकते हैं। यह जल्दी ही महसूस किया गया था कि कंप्यूटर के उपयोग से इस प्रकार के विश्लेषण में महत्वपूर्ण सहायता मिल सकती है। द लॉजिक थियोरिस्ट ने [[बर्ट्रेंड रसेल]] और [[अल्फ्रेड नॉर्थ व्हाइटहेड]] के सैद्धांतिक काम को गणितीय तर्क पर उनके प्रभावशाली काम में मान्य किया जिसे [[ गणितीय सिद्धांत ]] कहा जाता है। इसके अलावा, नए तार्किक प्रमेयों और प्रमाणों को मान्य करने और खोजने के लिए तार्किकों द्वारा बाद की प्रणालियों का उपयोग किया गया है।<ref>{{cite book|last=Newell|first=Allen|title=कंप्यूटर और विचार|chapter-url=https://archive.org/details/computersthought00feig|chapter-url-access=registration|year=1963|publisher=McGraw Hill|isbn=978-0262560924|pages=[https://archive.org/details/computersthought00feig/page/109 109–133] |author2=J.C. Shaw |author3=H.C. Simon|editor=Ed Feigenbaum|chapter=Empirical explorations with the logic theory machine}}</ref> | [[ कृत्रिम होशियारी ]] शब्द का उपयोग करने वाले पहले अनुप्रयोगों में से 1956 में [[एलन नेवेल]], जे.सी. शॉ और हर्बर्ट ए. साइमन द्वारा विकसित लॉजिक थिओरिस्ट सिस्टम था। उन निष्कर्षों (अतिरिक्त कथनों) को निकालें जो तर्क के नियमों द्वारा सत्य होने चाहिए। उदाहरण के लिए, यदि तार्किक प्रणाली दी गई है जो बताती है कि सभी मनुष्य नश्वर हैं और सुकरात मानव हैं तो मान्य निष्कर्ष यह है कि सुकरात नश्वर है। बेशक यह तुच्छ उदाहरण है। वास्तविक तार्किक प्रणालियों में कथन असंख्य और जटिल हो सकते हैं। यह जल्दी ही महसूस किया गया था कि कंप्यूटर के उपयोग से इस प्रकार के विश्लेषण में महत्वपूर्ण सहायता मिल सकती है। द लॉजिक थियोरिस्ट ने [[बर्ट्रेंड रसेल]] और [[अल्फ्रेड नॉर्थ व्हाइटहेड]] के सैद्धांतिक काम को गणितीय तर्क पर उनके प्रभावशाली काम में मान्य किया जिसे [[ गणितीय सिद्धांत ]] कहा जाता है। इसके अलावा, नए तार्किक प्रमेयों और प्रमाणों को मान्य करने और खोजने के लिए तार्किकों द्वारा बाद की प्रणालियों का उपयोग किया गया है।<ref>{{cite book|last=Newell|first=Allen|title=कंप्यूटर और विचार|chapter-url=https://archive.org/details/computersthought00feig|chapter-url-access=registration|year=1963|publisher=McGraw Hill|isbn=978-0262560924|pages=[https://archive.org/details/computersthought00feig/page/109 109–133] |author2=J.C. Shaw |author3=H.C. Simon|editor=Ed Feigenbaum|chapter=Empirical explorations with the logic theory machine}}</ref> | ||
== कंप्यूटर के लिए तर्क अनुप्रयोग == | == कंप्यूटर के लिए तर्क अनुप्रयोग == | ||
कृत्रिम बुद्धिमत्ता (एआई) के क्षेत्र में गणितीय तर्क का हमेशा से गहरा प्रभाव रहा है। क्षेत्र की शुरुआत से ही यह महसूस किया गया था कि तार्किक अनुमानों को स्वचालित करने की तकनीक में समस्याओं को हल करने और तथ्यों से निष्कर्ष निकालने की काफी क्षमता हो सकती है। रॉन ब्राचमैन ने प्रथम-क्रम तर्क (FOL) को मीट्रिक के रूप में वर्णित किया है जिसके द्वारा सभी AI ज्ञान प्रतिनिधित्व औपचारिकताओं का मूल्यांकन किया जाना चाहिए। एफओएल की तुलना में सूचना का वर्णन और विश्लेषण करने के लिए कोई अधिक सामान्य या शक्तिशाली ज्ञात विधि नहीं है। कंप्यूटर भाषा के रूप में केवल एफओएल का उपयोग नहीं करने का कारण यह है कि यह वास्तव में बहुत अभिव्यंजक है, इस अर्थ में कि एफओएल आसानी से बयान व्यक्त कर सकता है कि कोई भी कंप्यूटर, चाहे कितना शक्तिशाली हो, कभी भी हल नहीं कर सकता। इस कारण से प्रत्येक प्रकार का ज्ञान प्रतिनिधित्व किसी अर्थ में अभिव्यक्तता और संगणनीयता के | कृत्रिम बुद्धिमत्ता (एआई) के क्षेत्र में गणितीय तर्क का हमेशा से गहरा प्रभाव रहा है। क्षेत्र की शुरुआत से ही यह महसूस किया गया था कि तार्किक अनुमानों को स्वचालित करने की तकनीक में समस्याओं को हल करने और तथ्यों से निष्कर्ष निकालने की काफी क्षमता हो सकती है। रॉन ब्राचमैन ने प्रथम-क्रम तर्क (FOL) को मीट्रिक के रूप में वर्णित किया है जिसके द्वारा सभी AI ज्ञान प्रतिनिधित्व औपचारिकताओं का मूल्यांकन किया जाना चाहिए। एफओएल की तुलना में सूचना का वर्णन और विश्लेषण करने के लिए कोई अधिक सामान्य या शक्तिशाली ज्ञात विधि नहीं है। कंप्यूटर भाषा के रूप में केवल एफओएल का उपयोग नहीं करने का कारण यह है कि यह वास्तव में बहुत अभिव्यंजक है, इस अर्थ में कि एफओएल आसानी से बयान व्यक्त कर सकता है कि कोई भी कंप्यूटर, चाहे कितना शक्तिशाली हो, कभी भी हल नहीं कर सकता। इस कारण से प्रत्येक प्रकार का ज्ञान प्रतिनिधित्व किसी अर्थ में अभिव्यक्तता और संगणनीयता के मध्यका व्यापार है। भाषा जितनी अधिक अभिव्यंजक होती है, उतनी ही यह FOL के करीब होती है, इसके धीमे होने और अनंत लूप के लिए प्रवण होने की संभावना अधिक होती है।<ref>{{cite book|last=Levesque|first=Hector|title=ज्ञान प्रतिनिधित्व में पढ़ना|year=1985|publisher=Morgan Kaufmann|isbn=0-934613-01-X|page=[https://archive.org/details/readingsinknowle00brac/page/49 49]|author2=Ronald Brachman|editor=Ronald Brachman and Hector J. Levesque|chapter=A Fundamental Tradeoff in Knowledge Representation and Reasoning|quote=The good news in reducing KR service to theorem proving is that we now have a very clear, very specific notion of what the KR system should do; the bad new is that it is also clear that the services can not be provided... deciding whether or not a sentence in FOL is a theorem... is unsolvable.|chapter-url=https://archive.org/details/readingsinknowle00brac|url=https://archive.org/details/readingsinknowle00brac/page/49}}</ref> | ||
उदाहरण के लिए, विशेषज्ञ प्रणालियों में उपयोग किए जाने वाले IF THEN नियम FOL के बहुत सीमित उपसमुच्चय के करीब हैं। तार्किक संचालकों की पूरी श्रृंखला के साथ मनमाना सूत्रों के बजाय शुरुआती बिंदु वह है जिसे तर्कशास्त्री [[मूड सेट करना]] कहते हैं। नतीजतन, नियम-आधारित सिस्टम उच्च-प्रदर्शन गणना का समर्थन कर सकते हैं, खासकर यदि वे अनुकूलन एल्गोरिदम और संकलन का लाभ उठाते हैं।<ref>{{cite journal|last=Forgy|first=Charles|title=Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem*|journal=Artificial Intelligence|year=1982|volume=19|pages=17–37|url=http://web.yonsei.ac.kr/yusong/lecture/data/BI/Materials/1.1.Rete%20-%20A%20Fast%20Algorithm%20for%20the%20Many%20Pattern,%20Many%20Object%20Pattern%20Match%20Problem.pdf|access-date=25 December 2013|doi=10.1016/0004-3702(82)90020-0|archive-url=https://web.archive.org/web/20131227044049/http://web.yonsei.ac.kr/yusong/lecture/data/BI/Materials/1.1.Rete%20-%20A%20Fast%20Algorithm%20for%20the%20Many%20Pattern,%20Many%20Object%20Pattern%20Match%20Problem.pdf|archive-date=2013-12-27|url-status=dead}}</ref> | उदाहरण के लिए, विशेषज्ञ प्रणालियों में उपयोग किए जाने वाले IF THEN नियम FOL के बहुत सीमित उपसमुच्चय के करीब हैं। तार्किक संचालकों की पूरी श्रृंखला के साथ मनमाना सूत्रों के बजाय शुरुआती बिंदु वह है जिसे तर्कशास्त्री [[मूड सेट करना]] कहते हैं। नतीजतन, नियम-आधारित सिस्टम उच्च-प्रदर्शन गणना का समर्थन कर सकते हैं, खासकर यदि वे अनुकूलन एल्गोरिदम और संकलन का लाभ उठाते हैं।<ref>{{cite journal|last=Forgy|first=Charles|title=Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem*|journal=Artificial Intelligence|year=1982|volume=19|pages=17–37|url=http://web.yonsei.ac.kr/yusong/lecture/data/BI/Materials/1.1.Rete%20-%20A%20Fast%20Algorithm%20for%20the%20Many%20Pattern,%20Many%20Object%20Pattern%20Match%20Problem.pdf|access-date=25 December 2013|doi=10.1016/0004-3702(82)90020-0|archive-url=https://web.archive.org/web/20131227044049/http://web.yonsei.ac.kr/yusong/lecture/data/BI/Materials/1.1.Rete%20-%20A%20Fast%20Algorithm%20for%20the%20Many%20Pattern,%20Many%20Object%20Pattern%20Match%20Problem.pdf|archive-date=2013-12-27|url-status=dead}}</ref> | ||
तार्किक सिद्धांत के लिए अनुसंधान का अन्य प्रमुख क्षेत्र सॉफ्टवेयर इंजीनियरिंग था। [[ज्ञान आधारित सॉफ्टवेयर सहायक]] और प्रोग्रामर अपरेंटिस प्रोग्राम जैसी अनुसंधान परियोजनाओं ने सॉफ्टवेयर विनिर्देशों की शुद्धता को मान्य करने के लिए तार्किक सिद्धांत लागू किया। उन्होंने विभिन्न प्लेटफार्मों पर विशिष्टताओं को कुशल कोड में बदलने और कार्यान्वयन और विनिर्देश के | तार्किक सिद्धांत के लिए अनुसंधान का अन्य प्रमुख क्षेत्र सॉफ्टवेयर इंजीनियरिंग था। [[ज्ञान आधारित सॉफ्टवेयर सहायक]] और प्रोग्रामर अपरेंटिस प्रोग्राम जैसी अनुसंधान परियोजनाओं ने सॉफ्टवेयर विनिर्देशों की शुद्धता को मान्य करने के लिए तार्किक सिद्धांत लागू किया। उन्होंने विभिन्न प्लेटफार्मों पर विशिष्टताओं को कुशल कोड में बदलने और कार्यान्वयन और विनिर्देश के मध्यसमानता को साबित करने के लिए भी उनका उपयोग किया।<ref>{{cite journal|last=Rich|first=Charles|author2=Richard C. Waters |title=The Programmer's Apprentice Project: A Research Overview|journal=IEEE Expert |date=November 1987|url=ftp://publications.ai.mit.edu/ai-publications/pdf/AIM-1004.pdf|archive-url=https://web.archive.org/web/20170706115702/ftp://publications.ai.mit.edu/ai-publications/pdf/AIM-1004.pdf|url-status=dead|archive-date=2017-07-06|access-date=26 December 2013}}</ref> यह औपचारिक रूपान्तरण चालित दृष्टिकोण अक्सर पारंपरिक सॉफ्टवेयर विकास की तुलना में कहीं अधिक प्रयासपूर्ण होता है। हालांकि, उपयुक्त औपचारिकताओं और पुन: प्रयोज्य टेम्पलेट्स के साथ विशिष्ट डोमेन में दृष्टिकोण वाणिज्यिक उत्पादों के लिए व्यवहार्य साबित हुआ है। उपयुक्त डोमेन आमतौर पर वे होते हैं जैसे हथियार प्रणाली, सुरक्षा प्रणाली और वास्तविक समय वित्तीय प्रणाली जहां सिस्टम की विफलता में अत्यधिक उच्च मानव या वित्तीय लागत होती है। इस तरह के डोमेन का उदाहरण है [[ बड़े पैमाने पर एकीकरण ]] | वेरी लार्ज स्केल इंटीग्रेटेड (वीएलएसआई) डिजाइन- सीपीयू और डिजिटल उपकरणों के अन्य महत्वपूर्ण घटकों के लिए उपयोग किए जाने वाले चिप्स को डिजाइन करने की प्रक्रिया। चिप में त्रुटि विनाशकारी है। सॉफ्टवेयर के विपरीत, चिप्स को पैच या अपडेट नहीं किया जा सकता है। नतीजतन, यह साबित करने के लिए कि कार्यान्वयन विनिर्देश के अनुरूप है, औपचारिक तरीकों का उपयोग करने के लिए व्यावसायिक औचित्य है।<ref>{{cite book|last=Stavridou|first=Victoria|title=सर्किट डिजाइन में औपचारिक तरीके|year=1993|publisher=Press Syndicate of the University of Cambridge|isbn=0-521-443369|url=https://books.google.com/books?id=Hf_AZfW2YWsC&q=VLSI+chip+design+formal+methods&pg=PA14|access-date=26 December 2013}}</ref> | ||
कंप्यूटर प्रौद्योगिकी के लिए तर्क का अन्य महत्वपूर्ण अनुप्रयोग [[फ्रेम भाषा]]ओं और स्वचालित क्लासिफायरियर के क्षेत्र में रहा है। केएल-वन जैसी फ़्रेम भाषाओं में कठोर शब्दार्थ है। [[KL-ONE]] में परिभाषाओं को सिद्धांत और विधेय कलन को सेट करने के लिए सीधे मैप किया जा सकता है। यह किसी दिए गए मॉडल में सेट, सबसेट और संबंधों के | कंप्यूटर प्रौद्योगिकी के लिए तर्क का अन्य महत्वपूर्ण अनुप्रयोग [[फ्रेम भाषा]]ओं और स्वचालित क्लासिफायरियर के क्षेत्र में रहा है। केएल-वन जैसी फ़्रेम भाषाओं में कठोर शब्दार्थ है। [[KL-ONE]] में परिभाषाओं को सिद्धांत और विधेय कलन को सेट करने के लिए सीधे मैप किया जा सकता है। यह किसी दिए गए मॉडल में सेट, सबसेट और संबंधों के मध्यविभिन्न घोषणाओं का विश्लेषण करने के लिए विशेष प्रमेय साबित करने वालों को वर्गीकृत करने की अनुमति देता है। इस तरह मॉडल को मान्य किया जा सकता है और किसी भी असंगत परिभाषा को फ़्लैग किया जा सकता है। क्लासिफायरियर नई सूचनाओं का अनुमान भी लगा सकता है, उदाहरण के लिए मौजूदा सूचनाओं के आधार पर नए सेटों को परिभाषित करें और नए डेटा के आधार पर मौजूदा सेटों की परिभाषा बदलें। लचीलेपन का स्तर इंटरनेट की हमेशा बदलती दुनिया को संभालने के लिए आदर्श है। मौजूदा इंटरनेट पर तार्किक शब्दार्थ स्तर की अनुमति देने के लिए क्लासिफायर तकनीक को [[वेब ओन्टोलॉजी भाषा]] जैसी भाषाओं के शीर्ष पर बनाया गया है। की इस परत को [[सेमांटिक वेब]] कहा जाता है।<ref>{{cite journal|last=MacGregor|first=Robert|title=ज्ञान प्रतिनिधित्व को बढ़ाने के लिए विवरण वर्गीकरण का उपयोग करना|journal=IEEE Expert|date=June 1991|volume=6|issue=3|doi=10.1109/64.87683|pages=41–46|s2cid=29575443}}</ref><ref>{{cite journal|last=Berners-Lee |first=Tim |author2=James Hendler |author3=Ora Lassila |title=सिमेंटिक वेब वेब सामग्री का एक नया रूप जो कंप्यूटर के लिए सार्थक है, नई संभावनाओं की क्रांति लाएगा|journal=Scientific American |date=May 17, 2001 |url=http://www.cs.umd.edu/~golbeck/LBSC690/SemanticWeb.html |author-link=Tim Berners-Lee |doi=10.1038/scientificamerican0501-34 |volume=284 |pages=34–43 |url-status=dead |archive-url=https://web.archive.org/web/20130424071228/http://www.cs.umd.edu/~golbeck/LBSC690/SemanticWeb.html |archive-date=April 24, 2013 }}</ref> | ||
[[ लौकिक तर्क | लौकिक तर्क]] का इस्तेमाल कॉन्करेंसी (कम्प्यूटिंग) में रीजनिंग के लिए किया जाता है।<ref>{{cite conference | author = Colin Stirling | year = 1992 | title = मोडल और टेम्पोरल लॉजिक्स|pages=477–563| | [[ लौकिक तर्क | लौकिक तर्क]] का इस्तेमाल कॉन्करेंसी (कम्प्यूटिंग) में रीजनिंग के लिए किया जाता है।<ref>{{cite conference | author = Colin Stirling | year = 1992 | title = मोडल और टेम्पोरल लॉजिक्स|pages=477–563| | ||
book-title = Handbook of Logic in Computer Science |editor1=S. Abramsky |editor2=D. M. Gabbay |editor3=T. S. E. Maibaum | volume = II| publisher = Oxford University Press | isbn = 0-19-853761-1 }}</ref> | book-title = Handbook of Logic in Computer Science |editor1=S. Abramsky |editor2=D. M. Gabbay |editor3=T. S. E. Maibaum | volume = II| publisher = Oxford University Press | isbn = 0-19-853761-1 }}</ref> | ||
Revision as of 12:24, 21 May 2023
कंप्यूटर तर्क द्वार का आरेखीय प्रतिनिधित्व
कंप्यूटर विज्ञान में तर्क और कंप्यूटर विज्ञान के क्षेत्र के मध्य ओवरलैप को कवर करता है। विषय को अनिवार्य रूप से तीन मुख्य क्षेत्रों में विभाजित किया जा सकता है:
- सैद्धांतिक नींव और विश्लेषण।
- तर्कशास्त्रियों की सहायता के लिए कंप्यूटर प्रौद्योगिकी का उपयोग।
- कंप्यूटर अनुप्रयोगों के लिए तर्क से अवधारणाओं का उपयोग।
सैद्धांतिक नींव और विश्लेषण
तर्क कंप्यूटर विज्ञान में मौलिक भूमिका निभाता है। तर्क के कुछ प्रमुख क्षेत्र जो विशेष रूप से महत्वपूर्ण हैं, संगणना सिद्धांत (पूर्व में पुनरावर्तन सिद्धांत कहा जाता है), मॉडल तर्क और श्रेणी सिद्धांत हैं। अभिकलन का सिद्धांत अलोंजो चर्च और एलन ट्यूरिंग जैसे तर्कशास्त्रियों और गणितज्ञों द्वारा परिभाषित अवधारणाओं पर आधारित है।[1][2] चर्च ने सर्वप्रथम लैम्ब्डा-निश्चितता की अपनी धारणा का उपयोग करके एल्गोरिथम रूप से अघुलनशील समस्याओं का अस्तित्व दिखाया है। ट्यूरिंग ने प्रथम सम्मोहक विश्लेषण दिया जिसे यांत्रिक प्रक्रिया कहा जा सकता है और कर्ट गोडेल ने जोर देकर कहा कि उन्होंने ट्यूरिंग के विश्लेषण को सही पाया है।[3] इसके अतिरिक्त तर्क और कंप्यूटर विज्ञान के मध्य सैद्धांतिक ओवरलैप के कुछ अन्य प्रमुख क्षेत्र हैं:
- गोडेल की अपूर्णता प्रमेय यह साबित करती है कि अंकगणित की विशेषता के लिए पर्याप्त शक्तिशाली किसी भी तार्किक प्रणाली में ऐसे कथन होंगे जो उस प्रणाली के भीतर न तो सिद्ध किए जा सकते हैं और न ही अस्वीकृत। सॉफ्टवेयर की पूर्णता और शुद्धता को साबित करने की व्यवहार्यता से संबंधित सैद्धांतिक मुद्दों पर इसका सीधा अनुप्रयोग है।[4] *फ़्रेम की समस्या बुनियादी समस्या है जिसे आर्टिफिशियल इंटेलिजेंस एजेंट के लक्ष्यों और स्थिति का प्रतिनिधित्व करने के लिए पहले क्रम का तर्क का उपयोग करते समय दूर किया जाना चाहिए।[5]
- करी-हावर्ड पत्राचार तार्किक प्रणालियों और सॉफ्टवेयर के मध्य संबंध है। इस सिद्धांत ने प्रमाणों और कार्यक्रमों के मध्य सटीक पत्राचार स्थापित किया। विशेष रूप से यह दिखाया गया है कि सामान्य रूप से टाइप किए गए लैम्ब्डा-कैलकुलस में शब्द अंतर्ज्ञानवादी प्रस्तावपरक तर्क के प्रमाण के अनुरूप हैं।
- श्रेणी सिद्धांत गणित के दृष्टिकोण का प्रतिनिधित्व करता है जो संरचनाओं के मध्यसंबंधों पर जोर देता है। यह कंप्यूटर विज्ञान के कई पहलुओं से घनिष्ठ रूप से जुड़ा हुआ है: प्रोग्रामिंग भाषाओं के लिए टाइप सिस्टम, ट्रांज़िशन सिस्टम का सिद्धांत, प्रोग्रामिंग भाषाओं के मॉडल और प्रोग्रामिंग भाषा शब्दार्थ का सिद्धांत।[6]
तर्कशास्त्रियों की सहायता के लिए कंप्यूटर
कृत्रिम होशियारी शब्द का उपयोग करने वाले पहले अनुप्रयोगों में से 1956 में एलन नेवेल, जे.सी. शॉ और हर्बर्ट ए. साइमन द्वारा विकसित लॉजिक थिओरिस्ट सिस्टम था। उन निष्कर्षों (अतिरिक्त कथनों) को निकालें जो तर्क के नियमों द्वारा सत्य होने चाहिए। उदाहरण के लिए, यदि तार्किक प्रणाली दी गई है जो बताती है कि सभी मनुष्य नश्वर हैं और सुकरात मानव हैं तो मान्य निष्कर्ष यह है कि सुकरात नश्वर है। बेशक यह तुच्छ उदाहरण है। वास्तविक तार्किक प्रणालियों में कथन असंख्य और जटिल हो सकते हैं। यह जल्दी ही महसूस किया गया था कि कंप्यूटर के उपयोग से इस प्रकार के विश्लेषण में महत्वपूर्ण सहायता मिल सकती है। द लॉजिक थियोरिस्ट ने बर्ट्रेंड रसेल और अल्फ्रेड नॉर्थ व्हाइटहेड के सैद्धांतिक काम को गणितीय तर्क पर उनके प्रभावशाली काम में मान्य किया जिसे गणितीय सिद्धांत कहा जाता है। इसके अलावा, नए तार्किक प्रमेयों और प्रमाणों को मान्य करने और खोजने के लिए तार्किकों द्वारा बाद की प्रणालियों का उपयोग किया गया है।[7]
कंप्यूटर के लिए तर्क अनुप्रयोग
कृत्रिम बुद्धिमत्ता (एआई) के क्षेत्र में गणितीय तर्क का हमेशा से गहरा प्रभाव रहा है। क्षेत्र की शुरुआत से ही यह महसूस किया गया था कि तार्किक अनुमानों को स्वचालित करने की तकनीक में समस्याओं को हल करने और तथ्यों से निष्कर्ष निकालने की काफी क्षमता हो सकती है। रॉन ब्राचमैन ने प्रथम-क्रम तर्क (FOL) को मीट्रिक के रूप में वर्णित किया है जिसके द्वारा सभी AI ज्ञान प्रतिनिधित्व औपचारिकताओं का मूल्यांकन किया जाना चाहिए। एफओएल की तुलना में सूचना का वर्णन और विश्लेषण करने के लिए कोई अधिक सामान्य या शक्तिशाली ज्ञात विधि नहीं है। कंप्यूटर भाषा के रूप में केवल एफओएल का उपयोग नहीं करने का कारण यह है कि यह वास्तव में बहुत अभिव्यंजक है, इस अर्थ में कि एफओएल आसानी से बयान व्यक्त कर सकता है कि कोई भी कंप्यूटर, चाहे कितना शक्तिशाली हो, कभी भी हल नहीं कर सकता। इस कारण से प्रत्येक प्रकार का ज्ञान प्रतिनिधित्व किसी अर्थ में अभिव्यक्तता और संगणनीयता के मध्यका व्यापार है। भाषा जितनी अधिक अभिव्यंजक होती है, उतनी ही यह FOL के करीब होती है, इसके धीमे होने और अनंत लूप के लिए प्रवण होने की संभावना अधिक होती है।[8] उदाहरण के लिए, विशेषज्ञ प्रणालियों में उपयोग किए जाने वाले IF THEN नियम FOL के बहुत सीमित उपसमुच्चय के करीब हैं। तार्किक संचालकों की पूरी श्रृंखला के साथ मनमाना सूत्रों के बजाय शुरुआती बिंदु वह है जिसे तर्कशास्त्री मूड सेट करना कहते हैं। नतीजतन, नियम-आधारित सिस्टम उच्च-प्रदर्शन गणना का समर्थन कर सकते हैं, खासकर यदि वे अनुकूलन एल्गोरिदम और संकलन का लाभ उठाते हैं।[9] तार्किक सिद्धांत के लिए अनुसंधान का अन्य प्रमुख क्षेत्र सॉफ्टवेयर इंजीनियरिंग था। ज्ञान आधारित सॉफ्टवेयर सहायक और प्रोग्रामर अपरेंटिस प्रोग्राम जैसी अनुसंधान परियोजनाओं ने सॉफ्टवेयर विनिर्देशों की शुद्धता को मान्य करने के लिए तार्किक सिद्धांत लागू किया। उन्होंने विभिन्न प्लेटफार्मों पर विशिष्टताओं को कुशल कोड में बदलने और कार्यान्वयन और विनिर्देश के मध्यसमानता को साबित करने के लिए भी उनका उपयोग किया।[10] यह औपचारिक रूपान्तरण चालित दृष्टिकोण अक्सर पारंपरिक सॉफ्टवेयर विकास की तुलना में कहीं अधिक प्रयासपूर्ण होता है। हालांकि, उपयुक्त औपचारिकताओं और पुन: प्रयोज्य टेम्पलेट्स के साथ विशिष्ट डोमेन में दृष्टिकोण वाणिज्यिक उत्पादों के लिए व्यवहार्य साबित हुआ है। उपयुक्त डोमेन आमतौर पर वे होते हैं जैसे हथियार प्रणाली, सुरक्षा प्रणाली और वास्तविक समय वित्तीय प्रणाली जहां सिस्टम की विफलता में अत्यधिक उच्च मानव या वित्तीय लागत होती है। इस तरह के डोमेन का उदाहरण है बड़े पैमाने पर एकीकरण | वेरी लार्ज स्केल इंटीग्रेटेड (वीएलएसआई) डिजाइन- सीपीयू और डिजिटल उपकरणों के अन्य महत्वपूर्ण घटकों के लिए उपयोग किए जाने वाले चिप्स को डिजाइन करने की प्रक्रिया। चिप में त्रुटि विनाशकारी है। सॉफ्टवेयर के विपरीत, चिप्स को पैच या अपडेट नहीं किया जा सकता है। नतीजतन, यह साबित करने के लिए कि कार्यान्वयन विनिर्देश के अनुरूप है, औपचारिक तरीकों का उपयोग करने के लिए व्यावसायिक औचित्य है।[11] कंप्यूटर प्रौद्योगिकी के लिए तर्क का अन्य महत्वपूर्ण अनुप्रयोग फ्रेम भाषाओं और स्वचालित क्लासिफायरियर के क्षेत्र में रहा है। केएल-वन जैसी फ़्रेम भाषाओं में कठोर शब्दार्थ है। KL-ONE में परिभाषाओं को सिद्धांत और विधेय कलन को सेट करने के लिए सीधे मैप किया जा सकता है। यह किसी दिए गए मॉडल में सेट, सबसेट और संबंधों के मध्यविभिन्न घोषणाओं का विश्लेषण करने के लिए विशेष प्रमेय साबित करने वालों को वर्गीकृत करने की अनुमति देता है। इस तरह मॉडल को मान्य किया जा सकता है और किसी भी असंगत परिभाषा को फ़्लैग किया जा सकता है। क्लासिफायरियर नई सूचनाओं का अनुमान भी लगा सकता है, उदाहरण के लिए मौजूदा सूचनाओं के आधार पर नए सेटों को परिभाषित करें और नए डेटा के आधार पर मौजूदा सेटों की परिभाषा बदलें। लचीलेपन का स्तर इंटरनेट की हमेशा बदलती दुनिया को संभालने के लिए आदर्श है। मौजूदा इंटरनेट पर तार्किक शब्दार्थ स्तर की अनुमति देने के लिए क्लासिफायर तकनीक को वेब ओन्टोलॉजी भाषा जैसी भाषाओं के शीर्ष पर बनाया गया है। की इस परत को सेमांटिक वेब कहा जाता है।[12][13] लौकिक तर्क का इस्तेमाल कॉन्करेंसी (कम्प्यूटिंग) में रीजनिंग के लिए किया जाता है।[14]
यह भी देखें
संदर्भ
- ↑ Lewis, Harry R. (1981). संगणना के सिद्धांत के तत्व. Prentice Hall.
- ↑ Davis, Martin (11 May 1995). "Influences of Mathematical Logic on Computer Science". In Rolf Herken (ed.). यूनिवर्सल ट्यूरिंग मशीन. Springer Verlag. ISBN 9783211826379. Retrieved 26 December 2013.
- ↑ Kennedy, Juliette (2014-08-21). गोडेल की व्याख्या करना. Cambridge University Press. ISBN 9781107002661. Retrieved 17 August 2015.
- ↑ Hofstadter, Douglas R. (1999-02-05). Gödel, Escher, Bach: An Eternal Golden Braid. Basic Books. ISBN 978-0465026562.
- ↑ McCarthy, John; P.J. Hayes (1969). "कृत्रिम बुद्धि के दृष्टिकोण से कुछ दार्शनिक समस्याएं" (PDF). Machine Intelligence. 4: 463–502.
- ↑ Barr, Michael; Charles Wells (1998). कम्प्यूटिंग विज्ञान के लिए श्रेणी सिद्धांत (PDF). Centre de Recherches Mathématiques.
- ↑ Newell, Allen; J.C. Shaw; H.C. Simon (1963). "Empirical explorations with the logic theory machine". In Ed Feigenbaum (ed.). कंप्यूटर और विचार. McGraw Hill. pp. 109–133. ISBN 978-0262560924.
- ↑ Levesque, Hector; Ronald Brachman (1985). "A Fundamental Tradeoff in Knowledge Representation and Reasoning". In Ronald Brachman and Hector J. Levesque (ed.). ज्ञान प्रतिनिधित्व में पढ़ना. Morgan Kaufmann. p. 49. ISBN 0-934613-01-X.
The good news in reducing KR service to theorem proving is that we now have a very clear, very specific notion of what the KR system should do; the bad new is that it is also clear that the services can not be provided... deciding whether or not a sentence in FOL is a theorem... is unsolvable.
- ↑ Forgy, Charles (1982). "Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem*" (PDF). Artificial Intelligence. 19: 17–37. doi:10.1016/0004-3702(82)90020-0. Archived from the original (PDF) on 2013-12-27. Retrieved 25 December 2013.
- ↑ Rich, Charles; Richard C. Waters (November 1987). "The Programmer's Apprentice Project: A Research Overview" (PDF). IEEE Expert. Archived from the original (PDF) on 2017-07-06. Retrieved 26 December 2013.
- ↑ Stavridou, Victoria (1993). सर्किट डिजाइन में औपचारिक तरीके. Press Syndicate of the University of Cambridge. ISBN 0-521-443369. Retrieved 26 December 2013.
- ↑ MacGregor, Robert (June 1991). "ज्ञान प्रतिनिधित्व को बढ़ाने के लिए विवरण वर्गीकरण का उपयोग करना". IEEE Expert. 6 (3): 41–46. doi:10.1109/64.87683. S2CID 29575443.
- ↑ Berners-Lee, Tim; James Hendler; Ora Lassila (May 17, 2001). "सिमेंटिक वेब वेब सामग्री का एक नया रूप जो कंप्यूटर के लिए सार्थक है, नई संभावनाओं की क्रांति लाएगा". Scientific American. 284: 34–43. doi:10.1038/scientificamerican0501-34. Archived from the original on April 24, 2013.
- ↑ Colin Stirling (1992). "मोडल और टेम्पोरल लॉजिक्स". In S. Abramsky; D. M. Gabbay; T. S. E. Maibaum (eds.). Handbook of Logic in Computer Science. Vol. II. Oxford University Press. pp. 477–563. ISBN 0-19-853761-1.
अग्रिम पठन
- Ben-Ari, Mordechai (2012). Mathematical Logic for Computer Science (3rd ed.). Springer-Verlag. ISBN 978-1447141280.
- Harrison, John (2009). Handbook of Practical Logic and Automated Reasoning (1st ed.). Cambridge University Press. ISBN 978-0521899574.
- Huth, Michael; Ryan, Mark (2004). Logic in Computer Science: Modelling and Reasoning about Systems (2nd ed.). Cambridge University Press. ISBN 978-0521543101.
- Burris, Stanley N. (1997). Logic for Mathematics and Computer Science (1st ed.). Prentice Hall. ISBN 978-0132859745.
बाहरी संबंध
- Article on Logic and Artificial Intelligence at the Stanford Encyclopedia of Philosophy.
- IEEE Symposium on Logic in Computer Science (LICS)
- Alwen Tiu, Introduction to logic video recording of a lecture at ANU Logic Summer School '09 (aimed mostly at computer scientists)
