Изабель (помощник по пруфу) - Isabelle (proof assistant)
Автор (ы) оригинала | Lawrence Paulson |
---|---|
Разработчики) | Кембриджский университет и Технический университет Мюнхена и др. |
Первый выпуск | 1986 г. |
Стабильный выпуск | Isabelle2021 / февраль 2021 г .
|
Написано в | Стандартный ML и Scala |
Операционная система | Linux , Windows , macOS |
Тип | Математика |
Лицензия | Лицензия BSD |
Веб-сайт | Изабель |
Isabelle автоматизированная теорема доказывающая является логика высшего порядка (HOL) теорема доказывающая , написанная в Standard ML и Scala . Как средство доказательства теорем в стиле LCF , он основан на небольшом логическом ядре (ядре) для повышения надежности доказательств, не требуя - но поддерживающих - явных объектов доказательства.
Isabelle доступна в гибкой системной структуре, допускающей логически безопасные расширения, которые включают в себя как теории, так и реализации для генерации кода, документацию и конкретную поддержку множества формальных методов . В народе можно было бы сказать, что это « Затмение формальных методов». В последние годы значительное количество теорий и расширений системы было собрано в Архиве формальных доказательств Изабель ( Isabelle AFP ).
Лоуренс Полсон назвал Изабель в честь дочери Жерара Юэ .
Доказательство теорем Изабель - это бесплатное программное обеспечение , выпущенное под пересмотренной лицензией BSD .
Функции
Isabelle является универсальной: она предоставляет мета-логику (слабую теорию типов ), которая используется для кодирования логики объекта, такой как логика первого порядка (FOL), логика высшего порядка (HOL) или теория множеств Цермело – Френкеля (ZFC). Наиболее широко используемой объектной логикой является Isabelle / HOL, хотя значительные разработки теории множеств были завершены в Isabelle / ZF. Основной метод доказательства Изабель - это версия разрешения более высокого порядка , основанная на унификации более высокого порядка .
Несмотря на интерактивность, Isabelle имеет эффективные инструменты автоматического рассуждения, такие как механизм переписывания терминов и средство проверки таблиц , различные процедуры принятия решений, а также, через интерфейс автоматизации доказательства Sledgehammer, решатели теории внешней удовлетворяемости по модулю (SMT) (включая CVC4 ) и разрешение - основанные на автоматических средствах доказательства теорем (ATP), включая E и SPASS ( метод доказательства Metis восстанавливает доказательства разрешения, генерируемые этими ATP). Он также имеет два средства поиска моделей ( генераторы контрпримеров ): Nitpick и Nunchaku .
У Изабель есть локали, которые представляют собой модули, которые структурируют большие доказательства. Локаль фиксирует типы, константы и предположения в пределах указанной области, поэтому их не нужно повторять для каждой леммы .
Изар (« понятные полуавтоматические рассуждения ») - это формальный язык доказательств Изабель. Он вдохновлен системой Mizar .
Пример доказательства
Изабель позволяет писать доказательства в двух разных стилях: процедурном и декларативном . Процедурные доказательства определяют серию применяемых тактик ( функций / процедур доказательства теорем ); отражая процедуру, которую математик-человек может применить для доказательства результата, их обычно трудно читать, поскольку они не описывают результат этих шагов. Декларативные доказательства (поддерживаемые языком доказательств Изабель, Isar), с другой стороны, определяют фактические математические операции, которые должны быть выполнены, и, следовательно, их легче читать и проверять людьми.
Процедурный стиль устарел в последних версиях Isabelle.
Например, декларативное доказательство от противного в Isar того, что квадратный корень из двух не является рациональным, можно записать следующим образом.
theorem sqrt2_not_rational: "sqrt 2 ∉ ℚ" proof let ?x = "sqrt 2" assume "?x ∈ ℚ" then obtain m n :: nat where sqrt_rat: "¦?x¦ = m / n" and lowest_terms: "coprime m n" by (rule Rats_abs_nat_div_natE) hence "m^2 = ?x^2 * n^2" by (auto simp add: power2_eq_square) hence eq: "m^2 = 2 * n^2" using of_nat_eq_iff power2_eq_square by fastforce hence "2 dvd m^2" by simp hence "2 dvd m" by simp have "2 dvd n" proof - from ‹2 dvd m› obtain k where "m = 2 * k" .. with eq have "2 * n^2 = 2^2 * k^2" by simp hence "2 dvd n^2" by simp thus "2 dvd n" by simp qed with ‹2 dvd m› have "2 dvd gcd m n" by (rule gcd_greatest) with lowest_terms have "2 dvd 1" by simp thus False using odd_one by blast qed
Приложения
Изабель использовалась для помощи формальным методам спецификации, разработки и проверки программных и аппаратных систем.
Изабель использовалась для формализации множества теорем из математики и информатики , таких как теорема Гёделя о полноте, теорема Гёделя о непротиворечивости аксиомы выбора , теорема о простых числах , правильность протоколов безопасности и свойства семантики языков программирования . Многие из формальных доказательств, как уже упоминалось, хранятся в Архиве формальных доказательств, который содержит (по состоянию на 2019 год) не менее 500 статей с более чем 2 миллионами строк доказательств в общей сложности.
- В 2009 году проект L4.verified в NICTA представил первое формальное доказательство функциональной корректности ядра операционной системы общего назначения: микроядро seL4 (безопасное встроенное L4 ) . Доказательство построено и проверено в Isabelle / HOL и включает более 200000 строк сценария доказательства для проверки 7500 строк C. Проверка охватывает код, дизайн и реализацию, и основная теорема утверждает, что код C правильно реализует формальную спецификацию ядро. Доказательство выявило 144 ошибки в ранней версии C-кода ядра seL4 и около 150 проблем в каждой конструкции и спецификации.
- Определение языка программирования Lightweight Java было подтверждено типографским звуком в Isabelle.
Ларри Полсон ведет список исследовательских проектов], в которых используется Изабель.
Альтернативы
Несколько языков и систем предоставляют аналогичные функции:
- Agda , написанная на Haskell
- Coq , написанный на OCaml
- Lean , написано на C ++
- ЛЕГО
- Система Мицар
- Метамат
- Доказатель9
- Twelf , написано на стандартном ML
Примечания
использованная литература
дальнейшее чтение
- Лоуренс К. Полсон , "Основы универсального средства доказательства теорем" , Журнал автоматизированного мышления , том 5, выпуск 3 (сентябрь 1989 г.), страницы: 363–397, ISSN 0168-7433 .
- Лоуренс С. Полсон и Тобиас Нипкоу , «Учебное пособие для Изабель и руководство пользователя» , 1990.
- М.А. Озолс, К.А. Истофф и А. Кант, «DOVE: проверка и оценка , ориентированная на дизайн» , Труды AMAST 97 , М. Джонсон, редактор, Сидней, Австралия. Конспект лекций по информатике (LNCS) Vol. 1349, Springer Verlag, 1997.
- Тобиас Нипкоу, Лоуренс К. Полсон, Маркус Венцель, «Изабель / HOL - помощник по проверке логики высокого порядка» , 2020.