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