El demostrador automático de teoremas de Isabelle [a] es un demostrador de teoremas de lógica de orden superior (HOL) , escrito en ML estándar y Scala . Como demostrador de teoremas al estilo 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, 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 han recopilado un número sustancial de teorías y extensiones del sistema en el Archivo de Pruebas Formales de Isabelle ( Isabelle AFP ) [2]
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 cuenta con herramientas eficientes de razonamiento automático, 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 de teorías de módulo de satisfacibilidad externas (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). [4] También cuenta con dos buscadores de modelos ( contraejemplogeneradores): 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 semiautomático inteligible ") es el lenguaje de prueba formal de Isabelle. Está inspirado en el sistema Mizar . [5]