Cybernetics Wiki
Advertisement

Автоматическое доказательство теоремдоказательство теорем, реализуемое программно. В основе лежит аппарат математической логики. Используются идеи теории искусственного интеллекта. Процесс доказательства основывается на логике высказываний и логике предикатов.

Применение[]

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

Ссылки[]

Об автоматическом доказательстве теорем

Advertisement