Автоматическое доказательство теорем — доказательство теорем, реализуемое программно. В основе лежит аппарат математической логики. Используются идеи теории искусственного интеллекта. Процесс доказательства основывается на логике высказываний и логике предикатов.
Применение[]
В настоящее время автоматическое доказтельство теорем в промышленности применяется в основном при разработке и верификации интегральных схем. После того, как была обнаружена ошибка деления в процессорах Пентиум сложные модули операций с плавающей запятой современных микропроцессоров разрабатываются с особой тщательностью. В новых процессорах AMD, Intel и других фирм, автоматическое доказательство теорем используется для проверки что деление и другие операции выполняются корректно .
Ссылки[]
Об автоматическом доказательстве теорем
Эта страница использует содержимое раздела Википедии на русском языке. Оригинальная статья находится по адресу: Автоматическое доказательство теорем. Список первоначальных авторов статьи можно посмотреть в истории правок. Эта статья так же, как и статья, размещённая в Википедии, доступна на условиях CC-BY-SA .