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