Автоматическое доказательство теорем
Автоматическое
доказательство теорем, доказательство
теорем, реализуемое программно. В основе
лежит аппарат математической логики.
Используются идеи теории искусственного
интеллекта. Процесс доказательства
основывается на логике высказываний и
логике предикатов.
В настоящее время
автоматическое доказательство теорем
в промышленности применяется в основном
при разработке и верификации интегральных
схем. После того, как была обнаружена
ошибка деления в процессорах Pentium,
сложные модули операций с плавающей
запятой современных микропроцессоров
разрабатываются с особой тщательностью.
В новых процессорах AMD, Intel и других фирм
автоматическое доказательство теорем
используется для проверки того, что
деление и другие операции выполняются
корректно.