اثبات قضیه خودکار
اثبات قضیه خودکار در علوم رایانه به بررسی راه‌های ممکن برای اثبات قضیه‌ها به صورت خودکار (معمولاً با برنامه کامپیوتری) می‌پردازد. اثبات قضیه خودکار یکی از مهم‌ترین شاخه‌های استدلال خودکار به شمار می‌آید، اما همچنین به مقدار زیادی به علوم رایانه نظری و فلسفه مربوط است. منظور از قضیه در این‌جا قضیه ریاضی است.
آزمایشگاه ملی آرگون was a leader in automated theorem proving from the 1960s to the 2000s
نرم‌افزارهای اثبات قضیه خودکار قادرند برخی مسائل و قضایای ریاضی را اثبات نمایند و حتی در مواردی موفق به کشف اثبات‌های کوتاه‌تر برای برخی از قضایای ریاضی شده‌اند.
منابع
- (انگلیسی) Fitting، Melvin (۱۹۹۶). First-Order Logic and Automated Theorem Proving، ۲nd edition، Springer.