يرجى مراجعة هذه المقالة وإزالة وسم المقالات غير المراجعة، ووسمها بوسوم الصيانة المناسبة.

منطق آلي

من ويكيبيديا، الموسوعة الحرة
اذهب إلى التنقل اذهب إلى البحث
N write.svg
تعرَّف على طريقة التعامل مع هذه المسألة من أجل إزالة هذا القالب.هذه مقالة غير مراجعة. ينبغي أن يزال هذا القالب بعد أن يراجعها محرر مغاير للذي أنشأها؛ إذا لزم الأمر فيجب أن توسم المقالة بقوالب الصيانة المناسبة. يمكن أيضاً تقديم طلب لمراجعة المقالة في الصفحة المُخصصة لذلك. (يوليو 2018)

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

ومن أكثر المواضيع تطوراً في الاستدلال الآلي هي إثبات النظرية الآلية (حقل فرعي من المنطق الآلي والمنطق الرياضي الذي يتعامل مع إثبات النظريات الرياضية من خلال برامج الكمبيوتر) وإثبات التحقق الآلي، وقد ساهم أيضًا في في مجال الاحتمالات وتفسيرالمنطق.

ومن المواضيع المهمة التي تتضمن التفسير المنطقي في التنبؤ بالنتائج المستقبلية هو نظام الجدل الآلي، إذ كان هناك الكثير من القيود في موضوع الأستدلال الآلي، حيث أن نظام OSCAR لجون بولوك [1] هو مثال على نظام الجدل الآلي الذي من كونه أكثر من مجرد إثبات نظرية آلية.

تقنيات برامج المنطق الآلي تشمل المنطق الكلاسيكي ومنها المنطق العائم، وأيضًا الاستدلال البايزي وهو فرع من فروع الإحصاء.

تعريف وبدايات[عدل]

لعب تطوير المنطق الرياضي دورًا كبيرًا في مجال التفكير الآلي، والذي أدى بدوره إلى تطوير الذكاء الاصطناعي. التطوير المنطقي هو أن يتم التحقق من جميع الاستدلالات المنطقية إلي بديهيات أساسية في الرياضيات حيث يتم توفير جميع الخطوات المنطقية، دون استثناء. ولا يتم اللجوء إلى التخمين، لأن البراهين والدلالات أكثر منطقية وأقل عرضة للأخطاء المنطقية.[2] يشير البعض إلى اجتماع كورنيل الصيفي لعام 1957، الذي جمع عددًا كبيرًا من المتخصصين في علم الحاسوب وعلم الكمبيوتر، كأصل وبداية علم الاستدلال الآلي، أو الاستنتاج الآلي.[3] وينظر البعض الآخر أنه بدأ قبل ذلك مع برنامج المنطق 1955 من نيويل، شو وسيمون، أو مع تطبيق مارتن ديفيز لعام 1954 التي أثبتت أن (مجموع رقمين زوجي هو عدد زوجي).[4]

إن التفكير الآلي، على الرغم من كونه مجالًا كبيرًا وواسعا للأبحاث، مر بمرحلة "شتاء الذكاء الاصطناعي" في الثمانينيات والتسعينيات الأولى. لحسن الحظ، تم إنعاش هذا المجال. على سبيل المثال، في عام 2005 بدأت مايكروسوفت باستخدام تقنية التحقق في العديد من مشاريعها الداخلية ولضمان المواصفات المنطقية وفحص اللغة في الإصدار 2012 من Visual C.[3]

المساهمات المهمة[عدل]

كان Principia Mathematica أو المسمى بمبادئ الرياضيات عملًا بارزًا في المنطق الرسمي وهو كتاب من قبل ألفريد نورث وايتهيد وبيرتراند راسل، تمت كتابة الكتاب بغرض اشتقاق كل أو بعض التعبيرات الرياضية من حيث المنطق الرمزي. في البداية نُشر كتاب Principia Mathematica في ثلاثة مجلدات في 1910 و1912 و1913.[5]

المنظر المنهجي (LT) كان أول برنامج على الإطلاق تم تطويره في عام 1956 بواسطة ألن نيويل، هيربرت سيمون و كليف شاو "لتقليد المنطق البشري" وتم اختباره على اثنين وخمسين نظرية من الفصل الثاني من كتاب Principia Mathematica، ولقد أثبت البرنامج ثمانية وثلاثين من هذه النظريات[6]، ولقد وجد البرنامج دليلا على واحدة من النظريات التي قدمها وايتهيد وروسل. بعد محاولة فاشلة لنشر نتائجهم، ذكر نيويل، وشاو، وهربرت في نشرتهم عام 1958 في بحوث العمليات:

"هنالك الآن آلات عالمية تفكر، تتعلم وتنتج. وإضافة إلى ذلك، فإن قدرتها على القيام بهذه الأشياء ستزداد بسرعة حتى (في المستقبل القريب) فإن مدى حجم المشاكل التي يمكن أن تتعامل معها الآلة سوف تكون شاملة مع المدى الذي تم تطبيق العقل البشري فيه.”[7]

أمثلة على التطوير المنطقي

Year Theorem Proof System Formalizer Traditional Proof
1986 مبرهنات عدم الاكتمال لغودل Boyer-Moore Shankar[8] كورت غودل
1990 تقابل تربيعي Boyer-Moore Russinoff[9] غوتهولد أيزنشتاين
1996 المبرهنة الأساسية للتفاضل والتكامل HOL Light Harrison Henstock
2000 المبرهنة الأساسية في الجبر Mizar Milewski Brynski
2000 المبرهنة الأساسية في الجبر ديك Geuvers et al. Kneser
2004 مبرهنة الألوان الأربعة ديك Gonthier نيل روبرتسون et al.
2004 مبرهنة الأعداد الأولية Isabelle Avigad et al. أتل سيلبرغ-بول إيردوس
2005 مبرهنة منحنى جوردان HOL Light Hales Thomassen
2005 نظرية براور للنقطة الثابتة HOL Light Harrison Kuhn
2006 حدسية كيبلر Isabelle Bauer- Nipkow Hales
2007 Cauchy Residue HOL Light Harrison Classical
2008 مبرهنة الأعداد الأولية HOL Light Harrison analytic proof
2012 Feit-Thompson ديك Gonthier et al.[10] Bender, Glauberman and Peterfalvi
2016 Boolean Pythagorean triples problem Formalized as قابلية الإرضاء  [لغات أخرى] Heule et al.[11] none

أنظمة مثبتة[عدل]

نظرية بويرر مور المبرهنة (NQTHM).
تصميم NQTHM استلهم تنفيذة من قبل جون مكارثي وودي بيليدز.

بدأت في عام 1971 في أدنبره، اسكتلندا، وكان هذا برهان للنظرية بالكامل حيث طورت وصممت باستخدام لغة البرمجة ليسب. النقاط الرئيسية للـ NQTHM كانت:

  1. الاعتماد على مبدأ التعريف لوظائف التكرار الكاملة.
  2. الاستخدام المكثف لـ "التقييم الرمزي”.
  3. الاستدلال التعريفي على أساس فشل التقييم الرمزي.[12]
HOL Light
كتب بواسطة لغة كامل الموضوعية (الأو كامل)، ولقد تم تصميمه بطريقة منطقية بسيطة وتنفيذًا مرتب.
Coq
مساعد استدلال آلي صمم وطور في فرنسا، يمكن تلقائيا تطوير برامج قابلة للتنفيذ من خلال موصفاتها، إما بلغة البرمجة لغة كامل الموضوعية او هاسكل.تنفذ الخصائص والبرامج بنفس اللغة التي يطلق عليها حساب التفاضل والتكامل CIC.

التطبيقات[عدل]

تم استخدام التفكير الآلي بشكل أكثر انتشارا لإنشاء برامج آلية.

في كثير من الأحيان، تتطلب بعض التوجية البشري على أن تكون بعض هذه التوجيهات البشرية فعالة ومؤهلة بشكل عام كالاستدلالات الآلية. ومثال على ذلك Logic Theorist، جاء هذا البرنامج مع دليل على واحدة من النظريات في Principia Mathematica التي كانت أكثر كفاءة (تتطلب خطوات أقل) من الإثبات المقدم من وايتهيد ورسل.

نفذ تطبيق التفكير الآلي الحل لعدد متزايد من المشاكل في المنطق الرسمي، والرياضيات وعلوم الكمبيوتر، وبرمجة منطقية، والتحقق من البرامج والأجهزة، وتصميم الدوائر الكهربائية، وغيرها الكثير.

انظر أيضًا[عدل]

مجلات[عدل]

المراجع[عدل]

  1. ^ John L. Pollock
  2. ^ C. Hales, Thomas "Formal Proof", University of Pittsburgh. Retrieved on 2010-10-19 نسخة محفوظة 27 أغسطس 2018 على موقع واي باك مشين.
  3. أ ب "Automated Deduction (AD)", [The Nature of PRL Project]. Retrieved on 2010-10-19 نسخة محفوظة 01 مارس 2018 على موقع واي باك مشين.
  4. ^ Martin Davis, "The Prehistory and Early History of Automated Deduction," in Automation of Reasoning, eds. Siekmann and Wrightson, vol. 1, 1-28 at p. 15
  5. ^ "Principia Mathematica", at جامعة ستانفورد. Retrieved 2010-10-19 نسخة محفوظة 25 أغسطس 2018 على موقع واي باك مشين.
  6. ^ "The Logic Theorist and its Children". Retrieved 2010-10-18 نسخة محفوظة 03 نوفمبر 2017 على موقع واي باك مشين.
  7. ^ Shankar, Natarajan Little Engines of Proof, Computer Science Laboratory, معهد ستانفورد للأبحاث. Retrieved 2010-10-19 نسخة محفوظة 17 مايو 2008 على موقع واي باك مشين.
  8. ^ Shankar, N. (1994), Metamathematics, Machines, and Gödel's Proof, Cambridge, UK: Cambridge University Press, مؤرشف من الأصل في 17 ديسمبر 2019 الوسيط |CitationClass= تم تجاهله (مساعدة); الوسيط |separator= تم تجاهله (مساعدة)CS1 maint: ref=harv (link)
  9. ^ Russinoff, David M. (1992), "A Mechanical Proof of Quadratic Reciprocity", J. Autom. Reason., 8, صفحات 3–21, doi:10.1007/BF00263446 الوسيط |CitationClass= تم تجاهله (مساعدة); الوسيط |separator= تم تجاهله (مساعدة)CS1 maint: ref=harv (link)
  10. ^ Gonthier, G.; et al. (2013), "A Machine-Checked Proof of the Odd Order Theorem", in Blazy, S.; Paulin-Mohring, C.; Pichardie, D. (المحررون), Interactive Theorem Proving, 7998, صفحات 163–179, doi:10.1007/978-3-642-39634-2_14, ISBN 978-3-642-39633-5 الوسيط |CitationClass= تم تجاهله (مساعدة); الوسيط |separator= تم تجاهله (مساعدة)CS1 maint: ref=harv (link)
  11. ^ [1605.00723] Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer نسخة محفوظة 17 سبتمبر 2018 على موقع واي باك مشين.
  12. ^ The Boyer- Moore Theorem Prover. Retrieved on 2010-10-23 نسخة محفوظة 12 ديسمبر 2016 على موقع واي باك مشين.