Ядро верификатора в Isabelle / HOL

Вопрос

Каков основной алгоритм верификатора Isabelle / HOL?

Я ищу что-нибудь на уровне метациркулярного оценщика схем.

Разъяснение

Меня интересует только Verifier, а не стратегии автоматического доказательства теорем.

Контекст

Я хочу реализовать простой верификатор доказательства с нуля (исключительно в образовательных целях, а не для использования в производстве).

Я хочу понять основной алгоритм Verifier Isabelle / HOL. Меня не волнуют стратегии / код, используемый для автоматического доказательства теорем.

У меня есть подозрение, что основной алгоритм Verifier очень прост (и элегантен). Однако я не могу его найти.

Спасибо!


proof isabelle
person user1416711    schedule 05.02.2013    source источник

Ответы (2)


arrow_upward
11
arrow_downward

Изабель является членом «семейства LCF» средств проверки доказательств, что означает, что у вас есть специальный модуль - ядро ​​вывода, в котором выполняются все выводы для получения значений абстрактного типа данных thm. Это немного похоже на обработку системных вызовов ядром операционной системы. Все, что вы можете создать таким образом, «правильно по конструкции» относительно правильности реализации ядра. Поскольку среда языка программирования доказывающего устройства (Standard ML) имеет очень сильные статические свойства корректности типов, корректность по построению ядра вывода переносится на остальную часть реализации помощника доказательства, которая может быть довольно огромной.

Так что в принципе у вас есть относительно небольшая часть «доверенного ядра» и действительно большое «пользовательское пространство приложения». В частности, большая часть Isabelle / HOL на самом деле представляет собой большую коллекцию библиотечных теорий и дополнительных инструментов (в основном на SML) в пользовательской среде Isabelle.

В Isabelle инфраструктура ядра довольно сложна, но все же очень мала по сравнению с остальной частью системы. Фактически ядро ​​состоит из «микроядра» ( модуль Thm) и" нано-ядро "( модуль Context). Thm производит thm значений в смысле LCF-подхода Милнера, а Context заботится о theory сертификатах для любых результатов, которые вы производите, а также о контекстах доказательства для местных аргументов (особенно на языке доказательств Isar).

Если вы хотите узнать больше о пруверах в стиле LCF, я рекомендую посмотреть также HOL-Light, которая, вероятно, является самой маленькой реалистичной системой из семейства LCF, реалистичной в том смысле, что люди использовали ее для больших приложений. У HOL-Light есть большое преимущество в том, что его реализация может быть легко понятна, но этот минимализм также имеет некоторые недостатки: он не полностью защищает пользователя от бессмысленных действий в своей среде ML, которая представляет собой OCaml вместо SML. По различным техническим причинам OCaml по умолчанию не так "безопасен", как Standard ML.

person Makarius    schedule 28.02.2013
comment
Если вы хотите узнать больше о HOL-Light, загляните в Справочник. практической логики и автоматизированного мышления с помощью OCaml и < код href = "https://github.com/jack-pappas/fsharp-logic-examples/" rel = "nofollow noreferrer"> F #. - person Guy Coder; 01.03.2013

arrow_upward
2
arrow_downward

Если вы развернете исходники Изабель, например

http://isabelle.in.tum.de/dist/Isabelle2013_linux.tar.gz

вы найдете основные определения в

src / Pure / thm.ML

И уже есть такой проект, которым вы хотите заняться:

http://www.proof-technologies.com/holzero/

добавлено позже: другой, более серьезный проект

https://team.inria.fr/parsifal/proofcert/

person Gergely    schedule 28.02.2013