홀 라이트

HOL Light는 HOL 정리 프로버 패밀리의 일원입니다.다른 멤버와 마찬가지로 고전적인 고차 논리의 증명 보조입니다.다른 HOL 시스템에 비해 HOL Light는 비교적 단순한 기초가 되도록 설계되었습니다.HOL Light는 수학자이자 컴퓨터 과학자인 John Harrison에 의해 작성 및 관리되고 있습니다.HOL Light는 간이 BSD ^[1]라이선스로 출시됩니다.

논리적 기초

HOL Light는 유일한 원시 개념으로서 동등성을 갖는 유형 이론의 공식을 기반으로 합니다.추론의 기본 규칙은 다음과 같습니다.

$(\displaystyle\vdash t=t})$	리플	평등의 반사성
$({displaystyle\gamma\vdash s=t\qquad\Delta\vdash t=u}{\Gamma\cup\Delta\vdash s=u})$	트랜스	평등의 전이성
${\displaystyle {\Gamma\vdash f=g\qquad\Delta\vdash x=y}{\Gamma\cup\Delta\vdash f(x)=g(y)}}$	MK_COMB	평등의 일치
$(\displaystyle\Gamma\vdash s=t){\Gamma\vdash(\displayda x.s)=(\displayda x.t)}}$	ABS	평등 추상화( ${\displaystyle }${\$displaystyle$ x$}$는$in{\displaystyle \mathrm{}}$ {\$displaystyle \Gamma$ )에서 자유로울 수 없습니다.
${\displaystyle\vdash(\displayda x.t)x=t}$	베타.	추상화와 함수 응용의 연결
$(\displaystyle\displaystyle\qquad\{p\}\vdash p})$	추정하다	p$\displaystyle$p를 $가정$하여 p$\displaystyle$p를 $증명$합니다.
$(\displaystyle {\Gamma\vdash p=q\qquad\Delta\vdash p}{\Gamma\cup\Delta\vdash q})$	EQ_MP	평등과 공제 관계
$(\displaystyle {\Gamma \vdash p\qquad \Delta \vdash q}{\Gamma -\{q\})\cup (\Delta -\{p\})\vdash p=q}})$	차감_ANTISM_RULE	이원 추리에서 등식을 추론하다
${\displaystyle {\cfrac {x_{1},\ldots,x_{n}}\vdash p[x_{1},\ldots,x_{n}}{\Gamma [t_{1},\ldots,t_{n}}}}{\vdash p[t_{1}}}}}}$	인스톨	정리 가정과 결론에서 변수를 인스턴스화하다
${\displaystyle {\cfrac {Gamma [\alpha _{1},\alpha _{n}}\vdash p[\alpha _{1},\alpha _{n}}}{\Gamma [\tau _{1},\ldots _{n},\alpha _{n},\tau},\},$	INST_TYPE	정리 가정과 결론에서 유형 변수를 인스턴스화하다

유형 이론의 이 공식은 Lambek & Scott(1986) 섹션 II.2에 기술된 것과 매우 유사하다.

레퍼런스

• Lambek, J; Scott, P. J. (1986), Introduction to Higher Order Categorical logic, Cambridge University Press, ISBN 9780521356534

추가 정보

• Freek Wiedijk (December 2008), "Formal Proof — Getting Started" (PDF), Notices of the American Mathematical Society, 55 (11): 1408–1414, retrieved 2008-12-14

외부 링크

• 홀 라이트