Автоматическое доказательство

Автоматическое доказательство (англ. Automated Theorem Proving, ATP, а также Automated deduction) — доказательство, реализованное программно. В основе лежит аппарат математической логики. Используются идеи теории искусственного интеллекта. Процесс доказательства основывается на логике высказываний и логике предикатов.

В силу неразрешимости даже достаточно простых теорий практическое применение имеет лишь полуавтоматическое человеко-машинное доказательство. К тому же после полной автоматизации доказательство называют уже вычислением. Полностью автоматической может быть лишь проверка доказательства теорий посложнее (если его для этого подготовить).

Применение

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

Корпорация Microsoft использует автоматический доказатель теорем Z3 для верификации кода операционной системы Windows 7 и других программных продуктов^[1].

Примеры

• Agda
• Coq
• HOL
• Isabelle
• Idris
• Logic for Computable Functions
• Mercury
• Vampire^[англ.] — проект российских учёных, работающих в Манчестерском университете (Великобритания), 11 раз выигравший чемпионат мира среди систем доказательства.

См. также

• Машина вывода
• Экспертная система

Примечания

Ссылки

• Об автоматическом доказательстве теорем
• Система автоматизации дедукции (САД)
• SPASS: An Automated Theorem Prover for First-Order Logic with Equality
• Беклемишев Лев. FAQ: Компьютерные доказательства  (неопр.). postnauka.ru (20 мая 2014).

Эта страница в последний раз была отредактирована 24 декабря 2021 в 20:06.