Автоматизированный доказатель теорем Isabelle [a] — это средство доказательства теорем логики высшего порядка (HOL) , написанное на Standard ML и Scala . Как средство доказательства теорем в стиле LCF , оно основано на небольшом логическом ядре (ядре) для повышения надежности доказательств, не требуя — но поддерживая — явных объектов доказательства.
Isabelle доступна внутри гибкой системной структуры, допускающей логически безопасные расширения, которые включают в себя как теории, так и реализации для генерации кода, документации и конкретной поддержки различных формальных методов . Его можно рассматривать как IDE для формальных методов. В последние годы в Архиве формальных доказательств Изабель ( Isabelle AFP ) было собрано значительное количество теорий и системных расширений [2] .
Isabelle является общим: он обеспечивает металогику (слабую теорию типов ), которая используется для кодирования объектной логики, такой как логика первого порядка (FOL), логика высшего порядка (HOL) или теория множеств Цермело-Френкеля (ZFC). Наиболее широко используемой объектной логикой является Isabelle/HOL, хотя значительные разработки теории множеств были завершены в Isabelle/ZF. Основной метод доказательства Изабель — это версия разрешения более высокого порядка, основанная на объединении более высокого порядка .
Несмотря на интерактивность, Isabelle предлагает эффективные автоматические инструменты рассуждений, такие как механизм переписывания терминов и табличное доказательство , различные процедуры принятия решений, а также, через интерфейс автоматизации доказательств Sledgehammer , внешние решатели модульных теорий выполнимости (SMT) (включая CVC4 ) и разрешение . основанные на автоматических средствах доказательства теорем (ATP), включая E и SPASS ( метод доказательства Metis [b] восстанавливает доказательства разрешения, сгенерированные этими ATP). [4] Он также имеет два средства поиска моделей ( контрпримергенераторы): Nitpick [5] и Nunchaku . [6]
В Isabelle есть локали , которые представляют собой модули, структурирующие большие доказательства. Локаль фиксирует типы, константы и допущения в пределах указанной области видимости [5] , так что их не нужно повторять для каждой леммы .
Изар (« понятное полуавтоматическое рассуждение ») — это формальный язык доказательств Изабель. Он вдохновлен системой Mizar . [5]