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

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

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

Применение

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

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

Примеры

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