정의와 증명 구성
자료형과 재귀 함수, 귀납적 관계 등을 정의하고 성질을 증명한다. Isar는 증명의 구조를 텍스트로 드러내는 언어다. 명세와 증명이 같은 작업 환경 안에 있어 정의의 변경이 어떤 증명에 영향을 주는지 확인할 수 있다.
자동화 도구의 역할
단순화와 산술 추론 등 내장 기능을 이용하며 Sledgehammer를 통해 외부 증명기도 활용한다. 자동화는 증명 작업을 돕지만 어떤 명제가 필요한지와 어떤 가정을 둘지는 사용자가 정한다. 실패했다는 사실이 명제가 거짓임을 뜻하지는 않는다.
형식화 결과의 활용
실행 가능한 명세를 다른 프로그래밍 언어 코드로 생성하는 기능이 있다. 수학과 검증 응용을 모은 형식 증명 자료도 제공된다. 특정 결과를 사용할 때는 정의와 가정, 대상 논리와 버전을 함께 확인해야 한다.
관련 문서
HOL4 / Lean 증명 도구 / Lem 의미론 도구 / seL4