Автоматическое доказательство (, а также ) — доказательство, реализованное программно. В основе лежит аппарат математической логики. Используются идеи теории искусственного интеллекта. Процесс доказательства основывается на логике высказываний и логике предикатов.
В силу неразрешимости даже достаточно простых теорий практическое применение имеет лишь полуавтоматическое человеко-машинное доказательство. К тому же после полной автоматизации доказательство называют уже вычислением. Полностью автоматической может быть лишь проверка доказательства теорий посложнее (если его для этого подготовить).
Применение
В настоящее время автоматическое доказательство теорем в промышленности применяется в основном при разработке и верификации интегральных схем и программного обеспечения. После того, как была обнаружена ошибка деления в процессорах Пентиум, сложные модули операций с плавающей запятой современных микропроцессоров разрабатываются с особой тщательностью. В новых процессорах AMD, Intel и других фирм автоматическое доказательство теорем используется для проверки того, что деление и другие операции выполняются корректно.
Корпорация Microsoft использует автоматический доказатель теорем Z3 для верификации кода операционной системы Windows 7 и других программных продуктов.
Примеры
Agda Coq F*
HOL Isabelle Idris Lean (не связан с компанией LEGO) Logic for Computable Functions Mercury Mizar
— проект российских учёных, работающих в Манчестерском университете (Великобритания), 11 раз выигравший чемпионат мира среди систем доказательства.
См. также Инструмент интерактивного доказательства теорем Машина вывода Экспертная система
Примечания
Ссылки Об автоматическом доказательстве теорем Система автоматизации дедукции (САД) SPASS: An Automated Theorem Prover for First-Order Logic with Equality
Категория:Экспертные системы Категория:Формальные методы Категория:Автоматическое доказательство теорем