HOL Light es un miembro de la familia de probadores de teoremas HOL . Al igual que los otros miembros, es un asistente de prueba para la lógica clásica de orden superior . En comparación con otros sistemas HOL, HOL Light está diseñado para tener cimientos relativamente simples. HOL Light está escrito y mantenido por el matemático e informático John Harrison . HOL Light se lanza bajo la licencia BSD simplificada . [1]
Fundamentos lógicos
HOL Light se basa en una formulación de la teoría de tipos con la igualdad como única noción primitiva . Las reglas primitivas de inferencia son las siguientes:
REFL | reflexividad de la igualdad | |
TRANS | transitividad de la igualdad | |
MK_COMB | congruencia de igualdad | |
abdominales | abstracción de la igualdad no debe ser libre en ) | |
BETA | conexión de abstracción y aplicación de funciones | |
ASUMIR | asumiendo , probar | |
EQ_MP | relación de igualdad y deducción | |
DEDUCT_ANTISYM_RULE | deducir la igualdad a partir de la deducibilidad bidireccional | |
INST | instanciar variables en suposiciones y conclusión del teorema | |
INST_TYPE | instanciar variables de tipo en supuestos y conclusión del teorema |
Esta formulación de la teoría de tipos es muy cercana a la descrita en la sección II.2 de Lambek y Scott (1986) .
Referencias
- Lambek, J ; Scott, PJ (1986), Introducción a la lógica categórica de orden superior , Cambridge University Press, ISBN 9780521356534
Otras lecturas
- Freek Wiedijk (diciembre de 2008), "prueba formal - Para empezar" (PDF) , Avisos de la American Mathematical Society , 55 (11): 1408-1414 , recuperada 2008-12-14