Isabelle (ayudante de corrección)

Isabelle ^{[ a ],} un demostrador de teoremas automatizado, es un demostrador de teoremas de lógica de orden superior (HOL) , escrito en Standard ML y Scala . Como demostrador de teoremas de estilo Lógica para Funciones Computables (LCF), se basa en un pequeño núcleo lógico (kernel) para aumentar la confiabilidad de las pruebas sin requerir, aunque admitiendo, objetos de prueba explícitos.

Isabelle está disponible dentro de un marco de sistema flexible que permite extensiones lógicamente seguras, las cuales comprenden tanto teorías como implementaciones para la generación de código, la documentación y el soporte específico para una variedad de métodos formales . Puede considerarse un entorno de desarrollo integrado (IDE) para métodos formales. En los últimos años, se ha recopilado un número considerable de teorías y extensiones del sistema en el Archivo Isabelle de Pruebas Formales ( Isabelle AFP ). ^{[ 2 ]}

Isabelle fue nombrada por Lawrence Paulson en honor a la hija de Gérard Huet . ^{[ 3 ]}

El demostrador de teoremas Isabelle es software libre , publicado bajo la licencia BSD revisada .

Isabelle es genérica: proporciona una metalógica (una teoría de tipos débil ) que se utiliza para codificar lógicas de objetos como la lógica de primer orden (FOL), la lógica de orden superior (HOL) o la teoría de conjuntos de Zermelo-Fraenkel (ZFC). La lógica de objetos más utilizada es Isabelle/HOL, aunque importantes desarrollos de la teoría de conjuntos se completaron en Isabelle/ZF. El método de prueba principal de Isabelle es una versión de orden superior de la resolución , basada en la unificación de orden superior .

Aunque interactiva, Isabelle cuenta con eficientes herramientas de razonamiento automático, como un motor de reescritura de términos y un demostrador de tableaux , diversos procedimientos de decisión y, a través de la interfaz de automatización de pruebas Sledgehammer , solucionadores externos de satisfacibilidad módulo teorías (SMT) (incluido CVC4 ) y demostradores de teoremas automáticos (ATP) basados ​​en resolución , incluidos E , SPASS y Vampire (el método de prueba Metis ^{[ b ]} reconstruye las pruebas de resolución generadas por estos ATP). ^{[ 4 ]} También cuenta con dos buscadores de modelos ( generadores de contraejemplos ): Nitpick ^{[ 5 ]} y Nunchaku . ^{[ 6 ]}

Isabelle presenta locales que son módulos que estructuran demostraciones extensas. Un local fija tipos, constantes y supuestos dentro de un ámbito especificado ^{[ 5 ]} para que no tengan que repetirse para cada lema .

Isar (" razonamiento semiautomático inteligible ") es el lenguaje de prueba formal de Isabelle. Está inspirado en el sistema Mizar . ^{[ 5 ]}

Isabelle permite escribir demostraciones en dos estilos diferentes: el procedimental y el declarativo . Las demostraciones procedimentales especifican una serie de tácticas ( funciones/procedimientos de demostración de teoremas ) que se deben aplicar. Si bien reflejan el procedimiento que un matemático humano podría aplicar para demostrar un resultado, suelen ser difíciles de leer, ya que no describen el resultado de estos pasos. Este estilo se considera perjudicial en la documentación de Isabelle. ^{[ 7 ]}

Por otro lado, las demostraciones declarativas (respaldadas por el lenguaje de demostración de Isabelle, Isar) especifican las operaciones matemáticas reales que se deben realizar y, por lo tanto, son más fáciles de leer y verificar por los humanos.

Por ejemplo, una demostración declarativa por contradicción en Isar de que la raíz cuadrada de dos no es racional se puede escribir de la siguiente manera.

teorema sqrt2_not_rational: "sqrt 2 ∉ ℚ" prueba sea ?x = "sqrt 2" supongamos "?x ∈ ℚ" entonces obtenga mn :: nat donde sqrt_rat: "¦?x¦ = m / n" y lowest_terms: "coprime m n" por (regla Rats_abs_nat_div_natE) por lo tanto "m^2 = ?x^2 * n^2" por (auto simp add: power2_eq_square) por lo tanto eq: "m^2 = 2 * n^2" usando of_nat_eq_iff power2_eq_square por fastforce por lo tanto "2 dvd m^2" por simp por lo tanto "2 dvd m" por simp tiene "2 dvd n" prueba - de ‹2 dvd m› obtenga k donde "m = 2 * k" .. con eq tiene "2 * n^2 = 2^2 * k^2" por simp por lo tanto "2 dvd n^2" por simp así "2 dvd n" por simp qed con ‹2 dvd m› tiene "2 dvd gcd m n" por (rule gcd_greatest) con lowest_terms tiene "2 dvd 1" por simp así Falso usando odd_one por blast qed

Isabelle se ha utilizado para ayudar en los métodos formales de especificación, desarrollo y verificación de sistemas de software y hardware.

Isabelle se ha utilizado para formalizar numerosos teoremas de matemáticas e informática , como el teorema de completitud de Gödel , el teorema de Gödel sobre la consistencia del axioma de elección , el teorema de los números primos , la corrección de los protocolos de seguridad y las propiedades de la semántica de los lenguajes de programación . Muchas de las demostraciones formales se conservan, como se mencionó, en el Archivo de Demostraciones Formales, que contiene (a fecha de 2019) al menos 500 artículos con más de 2 millones de líneas de demostración en total. ^{[ 8 ]}

• En 2009, el proyecto L4.verified de NICTA produjo la primera prueba formal de corrección funcional de un núcleo de sistema operativo de propósito general: ^{[ 9 ]} el micronúcleo seL4 ( L4 integrado seguro ) . La prueba se construyó y verificó en Isabelle/HOL y comprende más de 200 000 líneas de script de prueba para verificar 7500 líneas de C. La verificación abarca el código, el diseño y la implementación, y el teorema principal establece que el código C implementa correctamente la especificación formal del núcleo. La prueba descubrió 144 errores en una versión temprana del código C del núcleo seL4, y alrededor de 150 problemas en cada uno de los aspectos de diseño y especificación.

• La definición del lenguaje de programación Lightweight Java fue probada como tipada en Isabelle. ^{[ 10 ]}

Varios lenguajes y sistemas ofrecen funciones similares:

• Agda , escrito en Haskell
• Rocq (anteriormente llamado Coq ), escrito en OCaml
• Lean , escrito en Lean y C++.
• LEGO , escrito en ML estándar de Nueva Jersey
• Sistema Mizar , escrito en Free Pascal.
• Metamath , escrito en ANSI C
• Prover9 , escrito en C , con una interfaz gráfica de usuario escrita en Python.
• Doce , escrito en Standard ML

• Sitio web oficial
• Isabelle en Stack Overflow
• El archivo de pruebas formales
• IsarMathLib