منطق محاسباتی

Computational Logic

مقطع: تحصیلات تکمیلی گرایش: الگوریتم‌ها و محاسبات
نوع درس: نظری تعداد واحد: ۳
پیش‌نیاز: – هم‌نیاز: –

هدف کلی

هدف از این درس ارایه سیستم‌های منطقی که در استدلال پیرامون ویژگی‌های سیستم‌های کامپیوتری به کار می‌روند از دیدگاهی محاسباتی و نظریه برهانی است. این سیستم‌های منطقی حداقل شامل منطق گزاره‌ای و منطق مرتبه اول استاندارد، حساب لامبدا، منطق‌های موجهات پایه، منطق‌های زمانی، منطق شهودی و منطق‌های خطی هستند که نحو، معناشناسی و نظام‌های استنتاج در آن‌ها از دیدگاه محاسباتی و با تاکید بر روش‌های اثبات خودکار قضایا (با تاکید کمتر بر روش وارسی مدل) ارائه می‌شوند. لازم است دانشجو به روشی مناسب (مانند تعریف پروژه‌های عملی) با برخی ابزارهای نرم‌افزاری موجود در اثبات خودکار قضایا و یاریگرهای اثبات و زبان‌های برنامه‌سازی مناسب این حوزه مانند ML و Lisp آشنا شود.

سرفصل‌ها

  1. مقدمه‌ای بر منطق محاسباتی
  2. منطق گزاره‌های کلاسیک
  3. نظریه‌های نحو، معناشناسی و نظام‌های استنتاجی
  4. روش‌های اثبات خودکار
  5. منطق گزاره‌های شهودی
  6. نظام‌های اصل موضوعی هیلبرتی
  7. منطق‌های موجهات گزاره‌ای
  8. منطق‌های زمانی گزاره‌ای
  9. مسئله وارسی الگو برای توصیفات منطق‌های زمانی
  10. منطق مرتبه اول کلاسیک
  11. قضایای صحت و تمامیت، قضایای حذف برش
  12. منطق خطی: دیدگاه محاسباتی و استنتاج خودکار قضایا

ارزیابی پیشنهادی

  • آزمون میان‌ترم (۲۵٪ کل نمره)
  • آزمون پایان‌ترم (۴۰٪ کل نمره)
  • حداقل شش سری تمرین (۲۵٪ کل نمره)
  • ارزش‌یابی مستمر در کلاس (۱۰٪ از نمره اصلی)

منابع پیشنهادی

  1. G. Boolos, J. Burgess, and R. Jeffrey. Computability and Logic. 5th Edition, Cambridge University Press, 2007.
  2. J. Goubault-Larrecq and I. Mackie. Proof Theory and Automated Deduction. Springer, 1997.
  3. J. H. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Dover Publications, 2015.
  4. M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach. 3rd Edition, Kluwer Academic Publishers, 2011.
  5. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.