El demostrador automatizado de teoremas de Isabelle [a] es un demostrador de teoremas interactivo , un demostrador de teoremas de lógica de orden superior (HOL) . Es un demostrador de teoremas al estilo LCF escrito en ML estándar . Por lo tanto, 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.
Autor (es) original (es) | Lawrence Paulson |
---|---|
Desarrollador (es) | Universidad de Cambridge y Universidad Técnica de Munich et al. |
Versión inicial | 1986 [1] |
Lanzamiento estable | Isabelle2020 / Abril 2020 |
Escrito en | ML estándar y Scala |
Sistema operativo | Linux , Windows , Mac OS X |
Tipo | Matemáticas |
Licencia | Licencia BSD |
Sitio web | isabelle |
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 . Popularmente se podría decir que es un « Eclipse de los métodos formales». En los últimos años, se han recopilado un número sustancial de teorías y extensiones del sistema en el Archivo de Pruebas Formales de Isabelle ( Isabelle AFP ) [2]
Características
Isabelle es genérica: proporciona una meta-lógica (una teoría de tipos débil ), que se utiliza para codificar lógicas de objetos como lógica de primer orden (FOL), lógica de orden superior (HOL) o teoría de conjuntos de Zermelo-Fraenkel (ZFC). La lógica de objetos más utilizada es Isabelle / HOL, aunque se completaron desarrollos significativos de la teoría de conjuntos en Isabelle / ZF. El principal método de prueba de Isabelle es una versión de resolución de orden superior, basada en unificación de orden superior .
Aunque interactiva, Isabelle presenta herramientas de razonamiento automático eficientes, como un motor de reescritura de términos y un probador de tableaux , 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 - basados experimentadores automatizados teorema (ATPs), incluyendo e y SPASS (los Metis [b] prueba método pruebas reconstruye resolución generados por estos ATPs). [3] También cuenta con dos buscadores de modelos ( generadores de contraejemplos ): Nitpick [4] y Nunchaku . [5]
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 [4] 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 . [4]
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 coherencia 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 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. [6]
El demostrador del teorema de Isabelle es un software gratuito , publicado bajo la licencia BSD revisada .
Isabelle fue nombrada por Lawrence Paulson en honor a la hija de Gérard Huet . [7]
Prueba de ejemplo
Isabelle permite que las pruebas se escriban en dos estilos diferentes, el procedimental y el declarativo . Las pruebas de procedimiento especifican una serie de tácticas ( funciones / procedimientos de prueba de teoremas ) para aplicar; si bien reflejan el procedimiento que un matemático humano podría aplicar para probar un resultado, generalmente son 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 procedimental ha quedado obsoleto en versiones recientes de Isabelle.
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 ∉ ℚ" demostración let ? x = "sqrt 2" asumir "? x ∈ ℚ" luego obtener mn :: nat donde sqrt_rat: "¦? x¦ = m / n" y lower_terms: "coprime mn " 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 tenga " 2 * n ^ 2 = 2 ^ 2 * k ^ 2 " por simp por tanto " 2 dvd n ^ 2 " por simp así " 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 tanto False usando odd_one por blast qed
Aplicaciones
Isabelle se ha utilizado para ayudar a métodos formales para la especificación, desarrollo y verificación de sistemas de software y hardware.
- En 2009, el proyecto L4.verified en NICTA produjo la primera prueba formal de la corrección funcional de un propósito general del núcleo del sistema operativo: [8] la SEL4 (Secure incrustado L4 ) microkernel . La prueba se construye y verifica en Isabelle / HOL y comprende más de 200,000 líneas de script de prueba para verificar 7,500 líneas de C.La verificación cubre 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 de el núcleo. La prueba descubrió 144 errores en una versión temprana del código C del kernel seL4, y alrededor de 150 problemas en cada diseño y especificación.
- La definición del lenguaje de programación de peso ligero de Java se comprobó tipo de sonido en Isabelle-. [9]
Larry Paulson mantiene una lista de proyectos de investigación que utilizan Isabelle.
Alternativas
Varios asistentes de prueba brindan una funcionalidad similar a Isabelle, que incluyen:
- Coq , sistema similar escrito en OCaml
- HOL , similar a la implementación de HOL de Isabelle
- Lean , sistema similar escrito en C ++
- Sistema Mizar
- Metamath
- Prover9
Notas
- ^ / ˌ ɪ z ə b ɛ l /
- ^ / M i t ɪ s /
Referencias
- ^ Paulson, LC (1986). "Deducción natural como resolución de orden superior". El diario de la programación lógica . 3 (3): 237. arXiv : cs / 9301104 . doi : 10.1016 / 0743-1066 (86) 90015-4 .
- ^ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. "Archivo de Pruebas Formales" . Consultado el 1 de mayo de 2021 .
- ^ Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow, "Prueba automática y refutación en Isabelle / HOL" , en: Cesare Tinelli, Viorica Sofronie-Stokkermans (eds.), Simposio internacional sobre fronteras de sistemas combinados - FroCoS 2011 , Springer, 2011 .
- ^ a b c Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich y Christoph Weidenbach, "Un marco de resolución de SAT verificado con aprendizaje, olvido, reinicio e incrementalidad" , Journal of Automated Reasoning 61 : 333–365 (2018).
- ^ Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli, "Model Finding for Recursive Functions in SMT" , en: Nicola Olivetti, Ashish Tiwari (eds.), VIII Conferencia conjunta internacional sobre razonamiento automatizado , Springer, 2016.
- ^ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. "Archivo de Pruebas Formales" . Consultado el 22 de octubre de 2019 .
- ^ Gordon, Mike (16 de noviembre de 1994). "1.2 Historia" . Isabelle y HOL . Cambridge AR Research (Grupo de razonamiento automatizado) . Consultado el 28 de abril de 2016 .
- ^ Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, junio; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (octubre de 2009). "seL4: verificación formal de un kernel del sistema operativo" (PDF) . 22º Simposio de ACM sobre principios de sistemas operativos . Big Sky, Montana, Estados Unidos. págs. 207–200.
- ^ Strniša, Rok; Parkinson, Matthew (7 de febrero de 2011). "Java ligero" . Archivo de pruebas formales (edición de febrero de 2011). ISSN 2150-914X . Consultado el 25 de noviembre de 2019 .
Otras lecturas
- Lawrence C. Paulson , "The Foundation of a Generic Theorem Prover" , Journal of Automated Reasoning , Volumen 5, Número 3 (septiembre de 1989), páginas: 363–397, ISSN 0168-7433 .
- Lawrence C. Paulson y Tobias Nipkow , "Isabelle Tutorial and User's Manual" , 1990.
- MA Ozols, KA Eastaughffe y A. Cant, "DOVE: Verificación y evaluación orientadas al diseño" , Actas de AMAST 97 , M. Johnson, editor, Sydney, Australia. Lecture Notes in Computer Science (LNCS) Vol. 1349, Springer Verlag, 1997.
- Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel, "Isabelle / HOL - A Proof Assistant for Higher-Order Logic" , 2020.
enlaces externos
- Sitio web de Isabelle
- Isabelle en Stack Overflow
- El archivo de pruebas formales
- IsarMathLib