Luz HOL

HOL Light es un asistente de demostración para lógica clásica de orden superior . Pertenece a la familia de demostradores de teoremas HOL . En comparación con otros sistemas HOL, HOL Light se caracteriza por tener fundamentos relativamente sencillos. HOL Light es obra del matemático e informático John Harrison, quien también se encarga de su mantenimiento. HOL Light se distribuye bajo la licencia BSD simplificada . ^{[ 1 ]}

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:

Esta formulación de la teoría de tipos es muy similar a la descrita en la sección II.2 de Lambek y Scott (1986) .

• Lambek, J .; Scott, P.J. (1986), Introducción a la lógica categórica de orden superior , Cambridge University Press, ISBN 9780521356534

• Freek Wiedijk (diciembre de 2008), "Demostración formal: primeros pasos" (PDF) , Notices of the American Mathematical Society , 55 (11): 1408–1414 , consultado el 14 de diciembre de 2008.

• Sitio web oficial