El demostrador automatizado de teoremas de 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 pequeño núcleo lógico (núcleo) para aumentar la confiabilidad de las pruebas sin requerir (aunque respaldar) objetos de prueba explícitos.
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, un número importante de teorías y ampliaciones de sistemas han sido recopiladas 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ébiles ), 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 en Isabelle/ZF se completaron importantes desarrollos en la teoría de conjuntos. El principal método de prueba de Isabelle es una versión de resolución de orden superior , basada en la unificación de orden superior .
Aunque interactiva, Isabelle presenta herramientas eficientes de razonamiento automático, como un motor de reescritura de términos y un probador de cuadros , varios procedimientos de decisión y, a través de la interfaz de automatización de pruebas Sledgehammer , solucionadores externos de teorías de módulo de satisfacibilidad (SMT) (incluido CVC4 ) y resolución . demostradores de teoremas automatizados (ATP) basados en E , SPASS y Vampire (el método de prueba de 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 pruebas grandes. Una configuración regional fija tipos, constantes y suposiciones dentro de un alcance específico [5] para que no tengan que repetirse para cada lema .
Isar (" razonamiento inteligible semiautomático ") es el lenguaje de prueba formal de Isabelle. Está inspirado en el sistema Mizar . [5]
Isabelle permite redactar pruebas en dos estilos diferentes, el procesal y el declarativo . Las pruebas procesales especifican una serie de tácticas ( funciones/procedimientos de demostración de teoremas ) a 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 (respaldadas por el lenguaje de prueba de Isabelle, Isar), por otro lado, especifican las operaciones matemáticas reales que se realizarán y, por lo tanto, los humanos las leen y verifican más fácilmente.
El estilo procesal ha quedado obsoleto en versiones recientes de Isabelle. [ cita necesaria ]
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 dejemos que ?x = "sqrt 2" asuma "?x ∈ ℚ" y luego obtenga mn :: nat donde sqrt_rat: "¦?x¦ = m / n" y lower_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 prueba de "2 dvd n" - de ‹2 dvd m› obtiene 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 por lo tanto "2 dvd n" por simp qed con ‹2 dvd m› tener "2 dvd gcd m n" por (regla gcd_greatest) con lower_terms tiene "2 dvd 1" por simp , por lo que es 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 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 del lenguaje de programación . Muchas de las pruebas formales, como se mencionó, se mantienen 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 Isabelle. [10]
Varios lenguajes y sistemas proporcionan una funcionalidad similar:
.svg/1280px-Free_and_open-source_software_logo_(2009).svg.png){kind=logo}