الاستدلال الآلي

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

أكثر المجالات الفرعية تطوراً في الاستدلال الآلي هي إثبات النظريات الآلي (والمجال الفرعي الأقل آلية ولكنه أكثر عملية وهو إثبات النظريات التفاعلي ) والتحقق الآلي من البراهين (الذي يُنظر إليه على أنه استدلال صحيح مضمون في ظل افتراضات ثابتة). كما أُنجزت أعمال واسعة النطاق في الاستدلال بالقياس باستخدام الاستقراء والاستنباط . ^{[ 1 ]}

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

تشمل أدوات وتقنيات الاستدلال الآلي المنطق والحسابات الكلاسيكية ، والمنطق الضبابي ، والاستدلال البايزي ، والاستدلال باستخدام أقصى إنتروبيا ، والعديد من التقنيات المخصصة الأقل رسمية.

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

لعب تطوير المنطق الصوري دورًا كبيرًا في مجال الاستدلال الآلي، الذي أدى بدوره إلى تطوير الذكاء الاصطناعي . البرهان الصوري هو برهانٌ تُدقَّق فيه كل استدلالات منطقية بالرجوع إلى البديهيات الأساسية للرياضيات. وتُقدَّم فيه جميع الخطوات المنطقية الوسيطة دون استثناء. ولا يُستعان بالحدس، حتى وإن كانت عملية تحويل الحدس إلى منطق روتينية. ولذلك، فإن البرهان الصوري أقل بديهية وأقل عرضةً للأخطاء المنطقية. ^{[ 6 ]}

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

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

كان كتاب "برينسيبيا ماثيماتيكا" عملاً بارزاً في المنطق الصوري ، من تأليف ألفريد نورث وايتهيد وبرتراند راسل . وكان هدفه اشتقاق جميع أو بعض التعبيرات الرياضية ، باستخدام المنطق الرمزي . نُشر "برينسيبيا ماثيماتيكا" في البداية في ثلاثة مجلدات في الأعوام 1910 و1912 و1913. ^{[ 9 ]} وقد جاء بعد كتاب "مبادئ الرياضيات " لبرتراند راسل ، الذي نُشر عام 1903، والذي عرض فيه راسل مفارقته الشهيرة، وناقش فيه فرضيته القائلة بأن الرياضيات والمنطق متطابقان.

كان برنامج Logic Theorist (LT) أول برنامج طُوِّر عام 1956 على يد ألين نيويل وكليف شو وهربرت أ. سيمون لمحاكاة التفكير البشري في إثبات النظريات، وقد طُبِّق على 52 نظرية من الفصل الثاني من كتاب Principia Mathematica، حيث أثبت 38 منها. ^{[ 10 ]} إضافةً إلى إثبات النظريات، وجد البرنامج برهانًا لإحدى النظريات كان أكثر أناقةً من البرهان الذي قدمه وايتهيد وراسل. بعد محاولة غير ناجحة لنشر نتائجهم، نشر نيويل وشو وهربرت بحثهم عام 1958 بعنوان " التقدم التالي في بحوث العمليات" .

"يوجد الآن في العالم آلات تفكر وتتعلم وتبدع. علاوة على ذلك، ستزداد قدرتها على القيام بهذه الأشياء بسرعة حتى (في مستقبل واضح) يصبح نطاق المشكلات التي يمكنها التعامل معها واسعًا مثل النطاق الذي تم تطبيقه على العقل البشري." ^{[ 11 ]}

أمثلة على البراهين الرسمية

سنة	نظرية	نظام إثبات	المُصاغ	الدليل التقليدي
1986	عدم الاكتمال الأول	بوير-مور	شانكار [ 12 ]	غودل
1990	التبادل التربيعي	بوير-مور	روسينوف [ 13 ]	أيزنشتاين
1996	أساسيات حساب التفاضل والتكامل	ضوء هول	هاريسون	هنستوك
2000	أساسيات الجبر	ميزر	ميليفسكي	برينسكي
2000	أساسيات الجبر	روك (ثم: كوك )	جيفرز وآخرون	كنيسر
2004	أربعة ألوان	روك (ثم: كوك )	غونتييه	روبرتسون وآخرون
2004	عدد أولي	إيزابيل	أفيغاد وآخرون	سيلبرغ - إردوش
2005	منحنى جوردان	ضوء هول	هيلز	توماسين
2005	نقطة ثابتة من براور	ضوء هول	هاريسون	كون
2006	فلايسبيك 1	إيزابيل	باور-نيبكو	هيلز
2007	بقايا كوشي	ضوء هول	هاريسون	كلاسيكي
2008	عدد أولي	ضوء هول	هاريسون	برهان تحليلي
2012	فيت-تومسون	روك (ثم: كوك )	غونتييه وآخرون [ 14 ]	بندر، جلوبرمان وبيترفالفي
2016	مسألة الأثلاث الفيثاغورية المنطقية	تمت صياغته رسمياً باسم اختبار SAT	هيول وآخرون [ 15 ]	لا أحد

برنامج إثبات نظرية بوير-مور (NQTHM)

استُلهم تصميم برنامج NQTHM من جون مكارثي ووودي بليدسو. بدأ تطويره عام ١٩٧١ في إدنبرة، اسكتلندا، وكان برنامجًا آليًا بالكامل لإثبات النظريات، بُني باستخدام لغة Pure Lisp . وتتمثل الجوانب الرئيسية لبرنامج NQTHM فيما يلي:

1. استخدام لغة ليسب كمنطق عملي.
2. الاعتماد على مبدأ التعريف للدوال التكرارية الكلية.
3. الاستخدام المكثف لإعادة الصياغة و"التقييم الرمزي".
4. استدلال استقرائي قائم على فشل التقييم الرمزي. ^{[ 16 ] [ 17 ]}

ضوء هول

تم تصميم HOL Light ، المكتوبة بلغة OCaml ، لتكون ذات أساس منطقي بسيط ونظيف، وتنفيذ غير معقد. وهي في جوهرها أداة مساعدة أخرى لإثبات صحة منطق الرتبة العليا الكلاسيكي. ^{[ 18 ]}

روك

يُعدّ برنامج Rocq ، الذي طُوّر في فرنسا، مساعدًا آليًا آخر لإثبات صحة البرامج، حيث يمكنه استخراج البرامج القابلة للتنفيذ تلقائيًا من المواصفات، سواءً كانت بلغة Objective CAML أو Haskell . وتُصاغ الخصائص والبرامج والإثباتات بلغة واحدة تُسمى حساب الإنشاءات الاستقرائية (CIC). ^{[ 19 ]}

يُستخدم الاستدلال الآلي بشكل شائع لبناء برامج إثبات النظريات الآلية. مع ذلك، غالبًا ما تتطلب هذه البرامج بعض التوجيه البشري لتكون فعّالة، ولذا تُصنّف عمومًا كمساعدين في البرهان . في بعض الحالات، ابتكرت هذه البرامج مناهج جديدة لإثبات نظرية ما. يُعدّ برنامج "Logic Theorist" مثالًا جيدًا على ذلك، حيث قدّم برهانًا لإحدى النظريات في كتاب "Principia Mathematica" كان أكثر كفاءة (يتطلب خطوات أقل) من البرهان الذي قدّمه وايتهيد وراسل. تُطبّق برامج الاستدلال الآلي لحلّ عدد متزايد من المشكلات في المنطق الصوري، والرياضيات، وعلوم الحاسوب، وبرمجة المنطق ، والتحقق من البرمجيات والأجهزة، وتصميم الدوائر ، وغيرها الكثير. تُعدّ مكتبة TPTP (سوتكليف وساتنر، 1998) مكتبةً لهذه المشكلات، ويتم تحديثها بانتظام. كما تُقام مسابقة بين برامج إثبات النظريات الآلية بانتظام في مؤتمر CADE (بيلتييه، سوتكليف وساتنر، 2002). يتم اختيار مسائل المسابقة من مكتبة TPTP. ^{[ 20 ]}

• التعلم الآلي الآلي (AutoML)
• إثبات النظريات آلياً
• مُستدل دلالي
• تحليل البرامج (علوم الحاسوب)
• تطبيقات الذكاء الاصطناعي
• نبذة عن الذكاء الاصطناعي
• علم الاستدلال القائم على الحالات • الاستدلال القائم على الحالات
• الاستدلال الاستنباطي
• محرك الاستدلال
• التفكير المنطقي السليم

• ورشة عمل دولية حول تطبيق المنطق
• سلسلة ورش عمل حول مواضيع ناجحة تجريبياً في مجال الاستدلال الآلي