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

 
== Автоматическая проверка доказательства ==
Доказательство может быть [[Автоматизированное доказательство|автоматизировано]] полностью лишь для очень небольшого круга простых теорий, поэтому важное значение получает его автоматическая проверка и для этого преобразование к проверяемому виду.
 
Для поддержания строгости за идеей проверки доказательства следует идея проверить эту проверку и так далее. Получившуюся бесконечную цепь проверок можно было бы свернуть, создав верифицирующий (проверяющий) себя верификатор, обладающий способностью развернуться до применимого на практике.
 
== См. также ==