المنطق في علوم الحاسوب

يركز المنطق دورًا أساسيًا في علوم الكمبيوتر. وفي بعض من المجالات الرئيسية للمنطق ذات الأهمية الكبرى وهي نظرية الحوسبة (التي كانوا يلقبونها سابقًا النظرية العودية) والمنطق المشروط ونظرية الفئة. وتعتمد نظرية الحساب على المفاهيم محددة من قبل المنطقيين وعلماء الرياضيات مثل العالم كنيسة ألونزو وألان تورينج.^[1][2] وقد أظهرت الكنيسة سابقا عن وجود مشاكل لا يمكن حلها خوارزميًا باستخدام مفهومه عن تعريف لامدا. ولقد أعطى عالم الحاسب الآن تورينج أول تحليل مقنع لما يمكن تسميته بالإجراء الميكانيكي وأكد الفيلسوف كورت جودل أنه قد وجد تحليل تورينج «مثاليًا».^[3] بالإضافة إلى بعض المجالات الرئيسية الأخرى للتداخل النظري بين المنطق وعلوم الكمبيوتر هي:

• وقد اثبت ان نظرية الفيلسوف جودل أنه لا يوجد أي نظام منطقي قوي بما يكفي لوصف الحساب ويحتوي على عبارات لا يمكن إثباتها أو ابطالها داخل هذا النظام. وهذا يتطلب تطبيق مباشر على القضايا النظرية المتعلقة بجدوى إثبات صحة البرنامج واكتماله.^[4]
• مشكلة الإطار وهي مشكلة أساسية يجب التغلب عليها عند استخدام منطق الدرجة الأولى لتمثيل أهداف وحالة عامل الذكاء الاصطناعي.^[5]
• المهندس كاري - هوارد هي علاقة توافق بين الأنظمة المنطقية والبرمجيات. وقد أنشأت هذه النظرية توافق المراسلات الدقيقة بين البراهين والبرامج. على وجه الخصوص، ولقد أظهر أن المصطلحات الواردة في حساب التفاضل والتكامل lambda-calculus وتتوافق مع براهين المنطق الحدسي الافتراضى.
• وقد مثلت نظرية الفئات وجهة نظرعلماء الرياضيات التي تؤكد على العلاقات بين الهياكل. ويرتبط ارتباطًا وثيقًا بالعديد من نواحي علوم الكمبيوتر منها: أنظمة نوع لغات البرمجة، ونظرية النظم الانتقالية، ونماذج لغات البرمجة، ونظرية دلالات لغة البرمجة.^[6]

كانت أحد الأعمال الأولى لاستخدام مصطلح الذكاء الاصطناعي هو نظام المنطقي الذي قد طوره الباحث Allen Newell والسياسي JC Shaw والعالم Herbert Simon في عام 1956. أحد الأشياء التي يقوم بها المنطق ولقد أخذ مجموعة من العبارات في المنطق والاستنتاج (عبارات إضافية) التي يجب أن تكون صحيحة بموجب قوانين المنطق. على سبيل المثال، إذا اخذت نظامًا منطقيًا ينص على أن «ان جميع البشر بشرا» و «سقراط بشر»، فإن الاستنتاج الصحيح هو «سقراط مميت». بالطبع هذا مثال سيء. وفي الأنظمة المنطقية الفعلية يمكن أن تكون العبارات كثيره ومعقدة. وقد أدرك موخرا أن هذا النوع من التحاليل يمكن أن تساعد بشكل كبير باستخدام أجهزة الكمبيوتر. وقد اثبت المنطق العمل النظري الفلاسفة لبرتراند راسل وألفريد نورث وايتهيد في عملهم الذي اثر على المنطق الرياضي المسمى Principia Mathematica . وبالإضافة إلى ذلك، لقد تم استخدام الأنظمة اللاحقة من قبل المنطقيين للتحقق منها واكتشاف النظريات والبراهين المنطقية الجديدة واكتشافها.^[7]

لطالما كان هناك بعض التأثيرات القويه من المنطق الرياضي في مجال الذكاء الاصطناعي (AI). ومنذ بداية المجال، قد تم إدراك أن التكنولوجيا قد بينت الاستدلالات المنطقية ويمكن أن يكون لها إمكانات كبيرة لحل الكثير من المشكلات واستخلاص النتائج من الحقائق. وقد صف رون براشمان منطق الدرجة الأولى (FOL) بأنه المقياس الذي يجب من خلاله تقييم جميع اشكال تمثيل المعرفة بالذكاء الاصطناعي. ولا توجد طريقة معروفة بشكل عام أو أكثر قوة لوصف وتحليل المعلومات من FOL. والسبب وراء عدم القدرة على استخدام لغة FOL كلغة للكمبيوتر هو أنها معبرة وأكثر تعقيدا في الواقع، بمعنى أن FOL يمكنها بسهولة التعبير عن عبارات لا يمكن لأي كمبيوتر تعبيرها، مهما كانت قوتها، اوحلها على الإطلاق. لهذا السبب فإن كل شكل من أشكال تمثيل المعرفة هو إلى حد ما مقايضة بين التعبيرية والحسابية. كلما كانت اللغة أكثر تعبيرًا وتفصيلا، كلما كانت أقرب إلى FOL ، زادت احتمالية أن تكون أبطأ وعرضة للدورة اللانهائية.^[8]

وعلى سبيل المثال، إذا كانت بعض القواعد المستخدمة في الأنظمة الخبيرة تتقارب مجموعة فرعية محدودة جدًا من FOL. لكن بدلاً من استخدام الصيغ التعسفية مع مجموعة كاملة من العوامل المنطقية، فإن نقطة البداية وهي ببساطة شديده ما يشير إليه المنطقيون باسم طريقة العمل. ونتيجة لذلك، يمكن للأنظمة المستندة إلى القواعد دعم الحساب عالي الأداء، وخاصة إذا قد استفادت من الخوارزميات والتحسين والتجميع.^[9]

ومجال هندسة البحث الآخر للنظرية المنطقية كان هندسة البرمجيات. وقد طبقت المشاريع البحثية مثل مساعد البرنامج القائم على المعرفة وبرامج للمتدربين وللمبرمجين النظرية المنطقية للتحقق من صحة مواصفات البرنامج. وكما انها قد استخدمتها لتحويل المواصفات إلى كود فعال ونشط على بعض المنصات المتنوعة لإثبات التكافؤ بين التنفيذ والمواصفات.^[10] وغالبًا ما يكون هذا النهج الرسمي القائم على التحول ويكون أكثر جهدًا بكثير من تطوير البرامج التقليدية. ومع ذلك، في بعض المجالات المحددة ذات الشكليات المناسبة والنماذج القابلة لإعادة الاستخدام، أثبت ان النهج قابل للتطبيق بالنسبة للمنتجات التجارية. عادة ما تكون المجالات المناسبة هي تلك الأنظمة، مثل أنظمة الأسلحة، والأنظمة الأمنية، والأنظمة المالية في الوقت الفعلي حيث يكون لفشل النظام تكلفة بشرية أو مالية باهظة الثمن. ومثال على هذا المجال هو تصميم متكامل واسع النطاق (VLSI) - وهي عملية تصميم الرقائق المستخدمة لوحدات المعالجة المركزية والمكونات الحيوية الأخرى لبعض الأجهزة الرقمية. وقد يكونخطأ واحد في الرقاقة كارثي. على عكس البرامج، لذا لا يمكن تصحيح الرقائق أو تحديثها. ونتيجة لذلك، هناك مبرر تجاري لاستخدام الأساليب الرسمية لإثبات أن التنفيذ يتوافق مع المواصفات.^[11]

وهنالك نطبيق آخر مهم للمنطق على تكنولوجيا الكمبيوتر كان في مجال لغات الإطار والمصنفات التلقائية. لغات الإطار مثل ais KL-ONE لها دلالات قويه. ويمكن تعيين التعاريف في KL-ONE مباشرة لوضع النظرية والحساب الأصلي. هذا يسمح لبرهنة النظرية المختصه تسمى مصنفات لتحليل الإعلانات المختلفة بين المجموعات الاساسيه والمجموعات الفرعية والعلاقات في نموذج محدد. وبهذه الطريقة يمكننا ان نتحقق من صحة النموذج ووضع علامة على أي تعريفات غير متناسقة. ويمكن أن نصنف أيضًا معلومات جديدة، على سبيل المثال تحديد مجموعات جديدة بناءً على المعلومات الموجودة وتغيير تعريف المجموعات الحالية بناءً على البيانات الجديدة. ومستوى المرونة المثالي للتعامل مع عالم الإنترنت الذي يتم تحديثه باستمرار. وقد تم تصميم تقنية Classifier على أساس لغات مثل Web Ontology Language للسماح بمستوى دلالي منطقي على الإنترنت الحالي. تسمى هذه الطبقة الويب الدلالي.^[12][13]

يستخدم المنطق الزمني للتفكير في الأنظمة المتزامنة.

• المنطق الآلي
• المنطق الحسابي
• البرمجة المنطقية

• Augusto، Luis M. (2017). Logical consequences. Theory and applications: An introduction. London: College Publications. ISBN:978-1-84890-236-7. مؤرشف من الأصل في 2019-09-28.
• Ben-Ari، Mordechai (2003). Mathematical Logic for Computer Science (ط. 2nd). Springer-Verlag]. ISBN:1-85233-319-7.
• Huth، Michael؛ Ryan، Mark (2004). Logic in Computer Science: Modelling and Reasoning about Systems (ط. 2nd). Cambridge University Press. ISBN:0-521-54310-X. مؤرشف من الأصل في 2006-07-09.
• Burris، Stanley N. (1997). Logic for Mathematics and Computer Science. Prentice Hall. ISBN:0-13-285974-2.

• مقالة عن المنطق والذكاء الاصطناعي في موسوعة ستانفورد للفلسفة.
• ندوة IEEE عن المنطق في علوم الكمبيوتر (LICS)
• Alwen Tiu ، مقدمة لتسجيل الفيديو المنطقي لمحاضرة في المدرسة الصيفية ANU Logic '09 (تستهدف في الغالب علماء الكمبيوتر)

• بوابة تقانة المعلومات
• بوابة علم الحاسوب
• بوابة فلسفة