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

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

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

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

يركز المنطق دورًا أساسيًا في علوم الكمبيوتر. وفي بعض من المجالات الرئيسية للمنطق ذات الأهمية الكبرى وهي نظرية الحوسبة (التي كانوا يلقبونها سابقًا النظرية العودية) والمنطق المشروط ونظرية الفئة . وتعتمد نظرية الحساب على المفاهيم محددة من قبل المنطقيين وعلماء الرياضيات مثل العالم كنيسة ألونزو وألان تورينج . [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]

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

انظر أيضا

المراجع
  1. Lewis, Harry R. Elements of the Theory of Computation. مؤرشف من R. Lewis الأصل تحقق من قيمة |مسار= (مساعدة) في 26 مايو 2020. الوسيط |CitationClass= تم تجاهله (مساعدة)
  2. Davis, Martin. "Influences of Mathematical Logic on Computer Science". In Rolf Herken (المحرر). The Universal Turing Machine. Springer Verlag. اطلع عليه بتاريخ 26 ديسمبر 2013. الوسيط |CitationClass= تم تجاهله (مساعدة)
  3. Kennedy, Juliette (2014-08-21). Interpreting Godel. Cambridge University Press. ISBN 9781107002661. مؤرشف من الأصل في 26 أبريل 2020. اطلع عليه بتاريخ 17 أغسطس 2015. الوسيط |CitationClass= تم تجاهله (مساعدة)
  4. Hofstadter, Douglas R. (1999-02-05). Gödel, Escher, Bach: An Eternal Golden Braid. Basic Books. ISBN 978-0465026562. مؤرشف من الأصل في 25 مارس 2020. الوسيط |CitationClass= تم تجاهله (مساعدة)
  5. McCarthy, J; P.J. Hayes (1969). "Some philosophical problems from the standpoint of artificial intelligence". Machine Intelligence. 4: 463–502. مؤرشف من الأصل في 25 مارس 2020. اطلع عليه بتاريخ أغسطس 2020. الوسيط |CitationClass= تم تجاهله (مساعدة); تحقق من التاريخ في: |تاريخ الوصول= (مساعدة)
  6. Barr, Michael; Charles Wells (1990). Category Theory for Computer. Prentice-Hall. الوسيط |CitationClass= تم تجاهله (مساعدة)
  7. 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 978-0262560924. الوسيط |CitationClass= تم تجاهله (مساعدة)
  8. Levesque, Hector; Ronald Brachman (1985). "A Fundamental Tradeoff in Knowledge Representation and Reasoning". In Ronald Brachman and Hector J. Levesque (المحرر). Reading in Knowledge Representation. Morgan Kaufmann. صفحة 49. ISBN 0-934613-01-X. مؤرشف من الأصل في 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. الوسيط |CitationClass= تم تجاهله (مساعدة)
  9. 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. الوسيط |CitationClass= تم تجاهله (مساعدة)
  10. Rich, Charles; Richard C. Waters (November 1987). "The Programmer's Apprentice Project: A Research Overview" (PDF). IEEE Expert. مؤرشف من الأصل (PDF) في 6 يوليو 2017. اطلع عليه بتاريخ 26 ديسمبر 2013. الوسيط |CitationClass= تم تجاهله (مساعدة)
  11. Stavridou, Victoria (1993). Formal Methods in Circuit Design. Press Syndicate of the University of Cambridge. ISBN 0-521-443369. مؤرشف من الأصل في 26 أبريل 2020. اطلع عليه بتاريخ 26 ديسمبر 2013. الوسيط |CitationClass= تم تجاهله (مساعدة)
  12. MacGregor, Robert (June 1991). "Using a description classifier to enhance knowledge representation". IEEE Expert. 6 (3): 41–46. doi:10.1109/64.87683. الوسيط |CitationClass= تم تجاهله (مساعدة)
  13. 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. اطلع عليه بتاريخ أغسطس 2020. الوسيط |CitationClass= تم تجاهله (مساعدة); تحقق من التاريخ في: |تاريخ الوصول= (مساعدة)

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

    روابط خارجية
    • بوابة علم الحاسوب
    • بوابة تقنية المعلومات
    This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.