اثبات‌یارها: توانایی‌ها و محدودیت‌ها

ارائه‌دهنده: مجتبی مجتهدی

اثبات‌یار، به یک ابزار نرم‌افزاری گفته می‌شود که کارش کمک به اثبات یک حکم است. حالا این حکم می‌تواند یک قضیه‌ی ریاضی باشد یا خاصیتی برای  برنامه‌ی نوشته شده در یک زبان برنامه‌نویسیِ دیگر باشد. از جمله اثبات‌یارهای معروف با جامعه‌ی کاربران زنده، می‌توان Coq, HOL Light, Isabelle  و ACL2 را نام برد. در این جلسه، می‌خواهیم به معرفی و بیان  توانایی‌ها و محدودیت‌های اثبات‌یارها بپردازیم.

چهارشنبه 5 اردیبهشت، ساعت 19 - باشگاه پایون