HOL Light, 어렵게 시작하지 마세요: 예제로 배우는 빠른 시작 가이드

HOL Light Tutorial

HOL Light 정리 증명기는 매뉴얼이 방대해 입문자가 흥미로운 작업을 하기 전에 소화해야 할 배경 지식이 많다. 이 튜토리얼은 단계별 예제를 통해 기본 사용법을 빠르게 익히도록 돕는 대안적 '퀵 스타트' 가이드다. 설치부터 OCaml 기초, 명제 논리, 방정식과 함수, 전술(tactics), 수 체계, 귀납적 정의, 실수 해석, 암호학(RSA), 양자역학의 Kochen-Specker 역설까지 폭넓게 다룬다. 일부 독자에게는 더 쉽게 받아들여질 수 있으며, 그렇지 않은 독자는 표준 매뉴얼을 참고하도록 안내한다.