Автоматическое доказательство теорем
Автоматическое доказательство теорем — доказательство теорем, реализуемое программно. В основе лежит аппарат математической логики. Используются идеи теории искусственного интеллекта. Процесс доказательства основывается на логике высказываний и логике предикатов.
Применение
В настоящее время автоматическое доказательство теорем в промышленности применяется в основном при разработке и верификации интегральных схем. После того, как была обнаружена ошибка деления в процессорах Пентиум, сложные модули операций с плавающей запятой современных микропроцессоров разрабатываются с особой тщательностью. В новых процессорах AMD, Intel и других фирм автоматическое доказательство теорем используется для проверки того, что деление и другие операции выполняются корректно.
См. также
Ссылки
- Об автоматическом доказательстве теорем
- Система Автоматизации Дедукции (САД)
- SPASS: An Automated Theorem Prover for First-Order Logic with Equality
de:Computerbeweis en:Automated theorem proving ja:自動定理証明 pl:Automatyczne dowodzenie twierdzeń
Если вам нравится SbUP.com Сайт, вы можете поддержать его - BTC: bc1qppjcl3c2cyjazy6lepmrv3fh6ke9mxs7zpfky0 , TRC20 и ещё....
