Если я правильно понимаю доказательство-обзорность или -слеживаемость, то по определению полностью подробное доказательство отслеживается на 100%, тогда как простое указание результата (например, леммы) отслеживается на 0%.
В этом случае я не понимаю, почему Lean лучше Coq, Isabelle или любого другого инструмента, основная цель которого - проверить правильность полностью подробного доказательства. Такие инструменты часто предоставляют средства для повышения автоматизации, что удобно, но, возможно, снижает отслеживаемость, в зависимости от того, как представлены дополнительные шаги проверки. Например. Тактика, подобная Coq, может повысить автоматизацию, но прослеживаемость может быть восстановлена, поскольку шаги, которые предполагает эта тактика, могут быть представлены таким же образом, как и явно предоставленные шаги: как приложения правил проверки или шаги дедукции.
Последняя часть сложна для шагов доказательства, предполагаемых SMT: решатели SMT могут достичь гораздо более высокой степени автоматизации, по сравнению с программами проверки доказательств, такими как Coq, но за счет прослеживаемости, потому что его рассуждения гораздо более технические и менее человеческие. / дедуктивный.
В качестве побочного замечания: эта разница между программами проверки правописания и решателями SMT напоминает мне разницу между классическим распознаванием изображений и распознаванием изображений на основе ИИ. Первый менее автоматизирован / эффективен, но его легче отследить / объяснить.
person
Malte Schwerhoff
schedule
01.09.2020
