Изабель (помощник по пруфу) - Isabelle (proof assistant)

Изабель
Изабель jedit.png
Isabelle / jEdit работает на macOS
Автор (ы) оригинала Lawrence Paulson
Разработчики) Кембриджский университет и Технический университет Мюнхена и др.
Первый выпуск 1986 г.
Стабильный выпуск
Isabelle2021 / февраль 2021 г . ; 8 месяцев назад ( 2021-02 )
Написано в Стандартный ML и Scala
Операционная система Linux , Windows , macOS
Тип Математика
Лицензия Лицензия BSD
Веб-сайт Изабель .in .tum .de

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 проблем в каждой конструкции и спецификации.

Ларри Полсон ведет список исследовательских проектов], в которых используется Изабель.

Альтернативы

Несколько языков и систем предоставляют аналогичные функции:

Примечания

использованная литература

дальнейшее чтение

внешние ссылки