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

تمثيل تخطيطي لبوابات منطق الكمبيوتر

يضم المنطق في علوم الحاسب التداخل بين مجالين مختلفين احدهما هومجال المنطق والاخر هومجال علوم الكمبيوتر . ويمكننا ان نقسم الموضوع إلى ثلاثة مجالات رئيسية وهي:

الأسس والتحليلات النظرية
يمكن استعمال الكمبيوتر لمساعده المنطقيين
يمكناستخدام المفاهيم من المنطق إلى تطبيقات الكمبيوتر

الأسس والتحليلات النظرية

يركز المنطق دورًا أساسيًا في علوم الكمبيوتر. وفي بعض من المجالات الرئيسية للمنطق ذات الأهمية الكبرى وهي نظرية الحوسبة (التي كانوا يلقبونها سابقًا النظرية العودية) والمنطق المشروط ونظرية الفئة . وتعتمد نظرية الحساب على المفاهيم محددة من قبل المنطقيين وفهماء الرياضيات مثل العالم كنيسة ألونزووألان تورينج . وقد أظهرت الكنيسة سابقا عن وجود مشاكل لا يمكن حلها خوارزميًا باستخدام مفهومه عن تعريف لامدا. ولقد منح عالم الحاسب الان تورينج أول تحليل مقنع لما يمكن تسميته بالإجراء الميكانيكي وأكد الفيلسوف كورت جودل أنه قد عثر تحليل تورينج "مثاليًا". بالإضافة إلى بعض المجالات الرئيسية الأخرى للتداخل النظري بين المنطق وعلوم الكمبيوتر هي:

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

أجهزة الكمبيوتر لمساعدة المنطقيين

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

تطبيقات المنطق لأجهزة الكمبيوتر

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

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

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

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

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

انظر أيضا

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

المراجع

^ Lewis, Harry R. . مؤرشف من R. Lewis الأصل تحقق من قيمة |مسار= (مساعدة) في 26 مايو2020.
^ Davis, Martin. "Influences of Mathematical Logic on Computer Science". In Rolf Herken (المحرر). The Universal Turing Machine. Springer Verlag. اطلع عليه بتاريخ 26 ديسمبر 2013.
^ Kennedy, Juliette (2014-08-21). . Cambridge University Press. ISBN . مؤرشف من الأصل في 26 أبريل 2020. اطلع عليه بتاريخ 17 أغسطس 2015.
^ Hofstadter, Douglas R. (1999-02-05). . Basic Books. ISBN . مؤرشف من الأصل في 25 مارس 2020.
^ McCarthy, J; P.J. Hayes (1969). "Some philosophical problems from the standpoint of artificial intelligence". Machine Intelligence. 4: 463–502. مؤرشف من الأصل في 25 مارس 2020.
^ Barr, Michael; Charles Wells (1990). Category Theory for Computer. Prentice-Hall.
^ Newell, Allen; J.C. Shaw; H.C. Simon (1963). "Empirical explorations with the logic theory machine". In Ed Feigenbaum (المحرر). Computers and Thought. McGraw Hill. صفحات 109–133. ISBN .
^ Levesque, Hector; Ronald Brachman (1985). "A Fundamental Tradeoff in Knowledge Representation and Reasoning". In Ronald Brachman and Hector J. Levesque (المحرر). . Morgan Kaufmann. صفحة 49. ISBN . مؤرشف من الأصل في 25 مارس 2020. 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. مؤرشف من الأصل (PDF) في 27 ديسمبر 2013. اطلع عليه بتاريخ 25 ديسمبر 2013.
^ Rich, Charles; Richard C. Waters (November 1987). "The Programmer's Apprentice Project: A Research Overview" (PDF). IEEE Expert. مؤرشف من الأصل (PDF) فيستة يوليو2017. اطلع عليه بتاريخ 26 ديسمبر 2013.
^ Stavridou, Victoria (1993). . Press Syndicate of the University of Cambridge. ISBN . مؤرشف من الأصل في 26 أبريل 2020. اطلع عليه بتاريخ 26 ديسمبر 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. مؤرشف من الأصل في 24 أبريل 2013.

قراءة متعمقة

Augusto, Luis M. (2017). . London: College Publications. ISBN . مؤرشف من الأصل في 28 سبتمبر 2019.
Ben-Ari, Mordechai (2003). Mathematical Logic for Computer Science (الطبعة 2nd). Springer-Verlag]. ISBN .
Huth, Michael; Ryan, Mark (2004). (الطبعة 2nd). Cambridge University Press. ISBN . مؤرشف من الأصل في 09 يوليو2006.
Burris, Stanley N. (1997). Logic for Mathematics and Computer Science. Prentice Hall. ISBN .

روابط خارجية

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