El demostrador de teoremas automatizado Isabelle [a] es un demostrador de teoremas de lógica de orden superior (HOL) , escrito en Standard ML y Scala . Como demostrador de teoremas de estilo LCF , se basa en un núcleo lógico pequeño (kernel) para aumentar la confiabilidad de las pruebas sin requerir objetos de prueba explícitos (aunque sí respaldarlos).
Isabelle está disponible dentro de un marco de sistema flexible que permite extensiones lógicamente seguras, que comprenden tanto teorías como implementaciones para la generación de código, documentación y soporte específico para una variedad de métodos formales . Puede verse como un IDE para métodos formales. En los últimos años, se ha recopilado una cantidad sustancial de teorías y extensiones de sistemas 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 del teorema de 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 se completaron importantes desarrollos de la teoría de conjuntos en Isabelle/ZF. El principal método de prueba de Isabelle es una versión de orden superior de la resolución , basada en la unificación de orden superior .
Aunque es interactiva, Isabelle cuenta con herramientas de razonamiento automático eficientes, como un motor de reescritura de términos y un probador de tablas , varios procedimientos de decisión y, a través de la interfaz de automatización de pruebas Sledgehammer , solucionadores de teorías de módulo de satisfacibilidad externa (SMT) (incluido CVC4 ) y probadores automatizados de teoremas basados en resolución (ATP), incluidos E , SPASS y Vampire (el método de prueba Metis [b] reconstruye 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 incluye configuraciones regionales , que son módulos que estructuran pruebas extensas. Una configuración regional fija tipos, constantes y suposiciones dentro de un alcance específico [5] de modo que no tengan que repetirse para cada lema .
Isar (« razonamiento semiautomático inteligible ») es el lenguaje de demostración formal de Isabelle. Está inspirado en el sistema Mizar . [5]
Isabelle permite escribir pruebas en dos estilos diferentes, el procedimental y el declarativo . Las pruebas 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. Las pruebas declarativas (apoyadas por el lenguaje de prueba de Isabelle, Isar), por otro lado, especifican las operaciones matemáticas reales que se deben realizar y, por lo tanto, son más fáciles de leer y verificar para los humanos.
El estilo procedimental ha quedado obsoleto en versiones recientes de Isabelle. [ cita requerida ]
Por ejemplo, una prueba 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" suponga "?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 ecuación tenemos "2 * n^2 = 2^2 * k^2" por simp por lo tanto "2 dvd n^2" por simp por lo tanto "2 dvd n" por simp qed con ‹2 dvd m› tenemos "2 dvd mcd m n" por (regla gcd_greatest) con lowest_terms tenemos "2 dvd 1" por simp por lo tanto Falso usando odd_one por blast qed
Isabelle se ha utilizado para ayudar a los métodos formales para la especificación, desarrollo y verificación de sistemas de software y hardware.
Isabelle se ha utilizado para formalizar numerosos teoremas de las matemáticas y la 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 pruebas formales se mantienen, como se mencionó, en el Archivo de Pruebas Formales, que contiene (a partir de 2019) al menos 500 artículos con más de 2 millones de líneas de prueba en total. [7]
Larry Paulson mantiene una lista de proyectos de investigación que utilizan a Isabelle. [10]
Varios idiomas y sistemas ofrecen una funcionalidad similar:
.svg/1280px-Free_and_open-source_software_logo_(2009).svg.png){kind=logo}