Лучшие вопросы
Таймлайн
Чат
Перспективы
Автоматическое доказательство
Из Википедии, свободной энциклопедии
Remove ads
Автоматическое доказательство (англ. Automated Theorem Proving, ATP, а также Automated deduction) — доказательство, реализованное программно. В основе лежит аппарат математической логики. Используются идеи теории искусственного интеллекта. Процесс доказательства основывается на логике высказываний и логике предикатов.
В силу неразрешимости даже достаточно простых теорий практическое применение имеет лишь полуавтоматическое человеко-машинное доказательство. К тому же после полной автоматизации доказательство называют уже вычислением. Полностью автоматической может быть лишь проверка доказательства теорий посложнее (если его для этого подготовить).
Remove ads
Применение
В настоящее время автоматическое доказательство теорем в промышленности применяется в основном при разработке и верификации интегральных схем и программного обеспечения. После того, как была обнаружена ошибка деления в процессорах Пентиум, сложные модули операций с плавающей запятой современных микропроцессоров разрабатываются с особой тщательностью. В новых процессорах AMD, Intel и других фирм автоматическое доказательство теорем используется для проверки того, что деление и другие операции выполняются корректно.
Корпорация Microsoft использует автоматический доказатель теорем Z3 для верификации кода операционной системы Windows 7 и других программных продуктов[1].
Remove ads
Примеры
- ACL2[англ.]
- Agda
- Coq
- F*
- HOL Light[англ.]
- HOL
- Isabelle
- Idris
- Lean
- LEGO[англ.] (не связан с компанией LEGO)
- Logic for Computable Functions
- Mercury
- Mizar
- Nqthm[англ.]
- NuPRL[англ.]
- PVS[англ.]
- Twelf[англ.]
- Vampire[англ.] — проект российских учёных, работающих в Манчестерском университете (Великобритания), 11 раз выигравший чемпионат мира среди систем доказательства.
См. также
Примечания
Ссылки
Wikiwand - on
Seamless Wikipedia browsing. On steroids.
Remove ads