مرقاة مِرقاةُ المنطق

التخصّص · حقلٌ من المنطق

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

برمجةُ المنطق والاستدلالُ الآلي، أي المنطقُ يُشغَّل: بُرولوغ، والحلّ، وقابليةُ الإشباع، وبراهينُ المبرهنات.

مدخلٌ مناسبٌ لـ علوم الحاسوب

المشكلة
أيَّ الأسئلة المنطقية تُجيب عنها الآلةُ آليًّا، وكيف نجعل الاستدلالَ نفسَه قابلًا للحوسبة؟
نقطةُ التحوّل
حسابُ لامدا عند تشرتش وعدمُ قابلية مسألة التوقّف للبتّ يحدِّدان الحدَّ الدقيق للاستدلال الآلي.
سؤالٌ مفتوح
إلى أيِّ مدًى تتوسّع حلّالاتُ SAT/SMT ومساعداتُ البرهان، وأتستطيع الآلةُ إيجادَ براهينَ جديدةٍ حقًّا؟

المتون

  • Church An Unsolvable Problem of Elementary Number Theory 1936
  • Lloyd Foundations of Logic Programming
  • Robinson & Voronkov Handbook of Automated Reasoning

لدراسته

  • Sterling & Shapiro The Art of Prolog
  • Fitting First-Order Logic and Automated Theorem Proving