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