논리 코어와 자동화
핵심 추론 체계를 간결하게 두고 그 위에 증명 절차와 라이브러리를 구성한다. 자동 도구와 이미 증명된 수학 정리를 이용하면 반복되는 작업을 줄일 수 있다. 새 도구를 만든다는 것과 임의의 명제를 참으로 받아들이는 것은 구분된다.
수학과 검증 응용
산술과 집합론, 실수 해석 등 수학적 기반을 다루며 부동소수점 알고리즘 검증과 큰 수학 형식화 작업에도 활용되었다. 이런 응용은 특정 정의와 성질에 대한 증명이며 모든 유사한 프로그램으로 보장이 자동 확대되지는 않는다.
다른 HOL 체계와 관계
HOL Light와 HOL4는 고차 논리 계열이지만 동일한 구현이나 호환되는 작업 환경은 아니다. 코드와 증명 라이브러리를 옮길 때는 표현과 도구 차이를 확인한다. 설치 조건은 사용하는 배포 버전의 안내를 기준으로 맞춘다.
관련 문서
HOL4 / Isabelle / Lean 증명 도구 / Rocq