منطق در علوم کامپیوتر
منطق در علوم کامپیوتر مباحث مشترک میان منطق و علوم کامپیوتر را پوشش می دهد. این موضوع را می توان به سه قسمت اصلی تقسیم کرد:
- مبانی نظری و آنالیز
- استفاده از فناوری کامپیوتر برای کمک به منطق دانان
- استفاده از مفاهیم منطق برای برنامه های کامپیوتری
مبانی نظری و آنالیز
منطق در علوم کامپیوتر نقش اساسی دارد. برخی از زمینه های اصلی منطق که قابل توجه هستند عبارت اند از: نظریه محاسبه پذیری (که قبلاً تئوری بازگشت نامیده می شد) ، منطق موجهات و نظریه رسته ها است . نظریه محاسبه بر اساس مفاهیمی که توسط منطق دانان و ریاضیدانانی مانند آلونزو چرچ و آلن تورینگ تعریف شده، بنا شده است. ابتدا چرچ با استفاده از ایده تعریف پذیری لامبدای خود وجود مسائل غیرقابل حل الگوریتمی را نشان داد. تورینگ اولین تحلیل قانع کننده از آنچه را که می توان یک روش مکانیکی نامید ارائه داد و کورت گودل ادعا کرد که او تحلیل تورینگ را "کامل" می داند. علاوه بر این، برخی از زمینه های دیگر در همپوشانی نظری بین منطق و علوم کامپیوتر عبارتند از:
- قضایای ناتمامیت گودل ثابت می کند که هر سیستم منطقی که توان لازم برای توصیف محاسبات را دارد شامل عبارت هایی است که داخل آن سیسام نه می توان آن ها را اثبات و نه رد کرد. این نکته به شکل مستقیم در مباحث نظری مربوط به امکان اثبات کامل بودن و درستی نرم‌افزار کاربرد دارد
- مشکل قاب یک مشکل اساسی است که باید هنگام استفاده از منطق مرتبه اول برای نشان دادن اهداف و وضعیت یک عامل هوش مصنوعی برطرف شود.
- مطابقت کاری-هوارد یک ارتباط میان سیستم های منطقی منطقی و نرم‌افزار است. این نظریه مطابقت دقیقی بین اثبات ها و برنامه ها ایجاد کرد. به ویژه نشان داد که اصطلاحات در جبر لاندا نوعدار-ساده با اثبات منطق گزاره ای شهودی مطابقت دارند
- نظریه رسته ها نشان دهنده نمایی از ریاضیات است که بر روابط بین ساختار ها تاکید دارد. این نظریه با بسیاری از جنبه های علوم کامپیوتر گره خورده است: انواع سیستم برای زبان های برنامه نویسی، نظریه سیستم های انتقالی، مدل های زبان برنامه نویسی و نظریه ی معنایی زبان برنامه نویسی.
کامپیوتر ها برای کمک به منطق دانان
یکی از اولین کاربرد های اصطلاح هوش مصنوعی سیستم نظریه پرداز منطق بود که در سال 1956 توسط آلن نیوول، جی سی شاو و هربرت سیمون توسعه یافت. یکی از کارهایی که منطق دانان انجام می دهند این است که مجموعه ای از گزاره ها(شرط ها) در منطق را در نظر می گیرند و مجموعه نتایجی (یا گزاره های جدیدی) را که با استفاده از قوانین منطق درست هستند استنباط می کنند. برای مثال اگر در یک سیستم منطقی که می گوید "همه انسان ها فانی هستند" و "سقراط انسان است" آنگاه استنتاج "سقراط فانی است" معتبر می باشد. البته این یک مثال بدیهی است. در سیستم های منطقی واقعی گزاره ها می توانند بسیار متعدد و پیچیدتر باشند. خیلی زود پی برده شد که در این تحلیل و بررسی ها می توان از کامپیوتر کمک قابل ملاحظه ای گرفت. سیستم نظریه پرداز منطق کار نظری برتراند راسل و آلفرد نورث وایتهد در کار تاثیر گذارشان در منطق ریاضی که مبادی ریاضیات نامیده میشد را تایید کرد. علاوه بر این متعاقباً از سیستم های بعدی توسط منطق دانان برای تایید و کشف نظریه ها و اثبات های منطقی جدید استفاده شد.
کاربرد های منطق برای کامپیوتر ها
همواره تاثیر زیادی از منطق ریاضی در زمینه هوش مصنوعی (AI) وجود داشته است. از ابتدا پی برده شد که فناوری خودکار کردن استنتاج های منطقی می تواند پتانسیل بسیار زیادی برای حل مسائل و نتیجه گیری از حقایق داشته باشد . ران برچمن منطق مرتبه اول (FOL) را به عنوان یک معیار توصیف کرده که تمام فرمالیته های دانش هوش مصنوعی باید توسط آن مورد بررسی قرار گرفته شوند. هیچ روش شناخته شده ایی کلی تر و قدرتمندتر از منطق مرتبه اول برای توصیف و تحلیل اطلاعات وجود ندارد. دلیل این که منطق مرتبه اول خود به سادگی به عنوان زبان کامپیوتر استفاده نمی‌شود این است که در واقع بیش از حد گویاست، به این معنا که منطق مرتبه اول می تواند به راحتی عبارت هایی را بیان کند که هیچ کامپیوتری، با هر توانی ، هرگز قادر به حل آن نمی‌باشد. به همین دلیل در هر روشی از نمایش دانش تا حدی یک معامله بین قابلیت تبیین و محاسبه پذیری وجود دارد. هر چه یک زبان قابلیت تبیین بالاتری داشته باشد به منطق مرتبه اول شبیه تر است و هر چه شباهت بیشتر باشد، این زبان احتمالاً کندتر و متمایل به یک حلقه ی بی نهایت است.
به عنوان مثال قوانین اگر آنگاه که در سیستم های خبره استفاده می شوند تقریباً یک زیر مجموعه ی محدود از منطق مرتبه اولند. به جای فرمول های دلخواه با طیف گسترده ای از عملگرهای منطقی ، نقطه شروع همان چیزی است که منطق دانان آن را قیاس استثنائی ذکر می کنند. در نتیجه، سیستم های قانون محور می توانند از محاسبات با کارایی بالا پشتیبانی کنند، به خصوص اگر از الگوریتم های بهینه سازی و تدوین استفاده کنند.
یکی دیگر از عمده زمینه های تحقیق برای نظریه منطق، مهندسی نرم‌افزار بود. پروژه های تحقیقاتی مانند دستیار نرم‌افزار دانش بنیان و برنامه های کارآموزی به برنامه نویسان از نظریه منطقی برای تایید درستی مشخصه نرم‌افزار استفاده کردند. همچنین از آنها برای تبدیل مشخصات به کد کارآمد در سیستم عامل های گوناگون و اثبات برابری میان پیاده سازی و مشخصات استفاده کردند. این روش رسمی مبتنی بر تبدیل، اغلب بسیار پر زحمت تر از توسعه نرم‌افزار سنتی است. اگر چه، در حوزه های خاص با فرم گرایی مناسب و الگوهایی با قابلیت استفاده مجدد، این روش برای محصولات تجاری ثابت شده است. دامنه های مناسب معمولاً مواردی از قبیل سیستم های تسلیحاتی، سیستم های امنیتی و سیستم های مالی درلحظه است که خرابی این سیستم هزینه های انسانی یا مالی بیش از حد دارد. نمونه ای از چنین دامنه ای طراحی یکپارچه مقیاس بزرگ است - فرایندیی برای طراحی تراشه های مورد استفاده در پردازنده ها و بقیه ی اجزای مهم دستگاه های دیجیتال. خطا در یک تراشه فاجعه بار است. بر خلاف نرم‌افزار، تراشه ها نمی‌توانند تعمیر یا به روز رسانی شوند. در نتیجه، توجیه تجاری برای استفاده از روش های رسمی برای اثبات مطابقت پیاده سازی و مشخصات وجود دارد.
یکی دیگر از کاربردهای مهم منطق در فناوری کامپیوتر در زمینه زبان های قاب و مرتب کننده های خودکار بوده است. زبان های قاب مانند کی ال-وان دارای مفاهیم سخت هستند. تعاریف موجود در کی ال-وان را می توان به طور مستقیم به نظریه مجموعه ها و ریاضیات گزاره ها مرتبط کرد. این نکته به اثبات کننده های تخصصی نظریه ها که مرتب کننده نامیده میشوند اجازه می دهد تا اظهارات مختلف بین مجموعه ها ، زیرمجموعه ها و روابط را در یک مدل داده شده تجزیه و تحلیل کنند. به این ترتیب مدل قابل اعتبارسنجی می باشد و هرگونه تعریف متناقضی پرچم گذاری می شود. مرتب کننده همچنین می تواند اطلاعات جدیدی را استنباط کند، برای مثال مجموعه های جدید را بر اساس اطلاعات موجود تعریف کند و یا تعریف مجموعه های موجود را بر اساس اطلاعات جدید تغییر دهد. این سطح انعطاف پذیری برای اداره کردن دنیای همیشه در حال تغییر اینترنت ایدئال است. فناوری مرتب کننده بر روی زبانهایی مانند زبان هستی شناسی وب سوار شده تا بتواند از سطح منطق معناشناسی به اینترنت موجود دسترسی پیدا کند. این لایه وب معنایی نامیده می شود.
منطق زمانی برای استدلال در سیستم های همزمان استفاده می شود .
جستارهای وابسته
منابع
- ↑ McCarthy, J; P.J. Hayes (1969). "Some philosophical problems from the standpoint of artificial intelligence". Machine Intelligence. 4: 463–502. Archived from the original on 25 March 2020. Retrieved 22 November 2020.
- ↑ 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. Retrieved 26 December 2013.
- ↑ MacGregor, Robert (June 1991). "Using a description classifier to enhance knowledge representation". IEEE Expert. 6 (3): 41–46. doi:10.1109/64.87683.
- ↑ Berners-Lee, Tim; James Hendler; Ora Lassila (May 17, 2001). "The Semantic Web A new form of Web content that is meaningful to computers will unleash a revolution of new possibilities". Scientific American. 284: 34–43. doi:10.1038/scientificamerican0501-34. Archived from the original on April 24, 2013.
خواندن بیشتر
- Ben-Ari, Mordechai (2003). Mathematical Logic for Computer Science (2nd ed.). Springer-Verlag]. ISBN 1-85233-319-7.
- Huth, Michael; Ryan, Mark (2004). Logic in Computer Science: Modelling and Reasoning about Systems (2nd ed.). Cambridge University Press. ISBN 0-521-54310-X.
- Burris, Stanley N. (1997). Logic for Mathematics and Computer Science. Prentice Hall. ISBN 0-13-285974-2.
پیوند به بیرون
- 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)