Описание тега theorem-proving

Доказательство теорем, в настоящее время наиболее развитая область автоматизированных рассуждений, - это доказательство математических теорем с помощью компьютерной программы.

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

В контексте программирования средства доказательства теорем все больше влияют на разработку языков программирования и методов проверки правильности программ.