Формальная верификация: различия между версиями

Метка: редактор вики-текста 2017
 
== Автоматическая проверка доказательства ==
Доказательство может быть [[Автоматизированное доказательство|автоматизировано]] полностью лишь для очень небольшого круга простых теорий, поэтому важное значение получает его автоматическая проверка и для этого преобразование к проверяемому виду. {{Источник}}
 
Для поддержания строгости при проверке доказательства верификатором следует проверить ещё и верификатор, для чего нужен ещё один верификатор и так далее. Получившуюся бесконечную цепь верификаторов можно было бы свернуть, построив верифицирующий себя верификатор, обладающий способностью развернуться до применимого на практике.