El tutorial de HOL Light que promete enseñarte a demostrar teoremas sin perderte en el manual
HOL Light Tutorial
HOL Light es un potente demostrador de teoremas, pero su manual resulta intimidante por la gran cantidad de conocimientos previos que exige. Este tutorial ofrece una guía de inicio rápido con ejemplos graduados para aprender lo básico del sistema de forma práctica. Cubre desde la instalación en Windows, Linux o macOS hasta temas avanzados como tácticas personalizadas, tipos de datos inductivos y la formalización de la paradoja de Kochen-Specker.
El demostrador de teoremas HOL Light puede ser difícil de empezar a usar. Aunque el manual es bastante detallado y completo, la gran cantidad de información de fondo que hay que absorber antes de que el usuario pueda hacer algo interesante resulta intimidante.