ابزارهای اثبات‌سازی

1 مقاله

لگو: دستیار اثبات‌سازی

لگو یک دستیار اثبات‌سازی است که توسط رندی پولاک در دانشگاه ادینبرو توسعه یافته است. این ابزار، نظریه‌های نوع مختلفی را پیاده‌سازی می‌کند، از جمله چارچوب منطقی ادینبرو، حساب ساخت‌ها، حساب ساخت‌های تعمیم‌یافته و نظریه یکپارچه انواع وابسته.

8 تیر 1405