HOL Light

HOL Light is член семейства устройств доказательства теорем HOL. Как и другие элементы, это помощник по проверке для классической логики более высокого порядка. По сравнению с другими системами HOL, HOL Light имеет относительно простую основу. HOL Light создан и поддерживается математиком и компьютерным ученым. HOL Light выпущен под упрощенной лицензией BSD.

• 1 Логические основы
• 2 Ссылки
• 3 Дополнительная литература
• 4 Внешние ссылки

HOL Light основан на формулировке теории типов с равенством как единственным примитивным понятием. Примитивные правила вывода следующие:

$⊢\; t\; =\; t\; \{\backslash \; displaystyle\; \{\backslash \; cfrac\; \{\backslash \; qquad\}\; \{\backslash \; vdash\; t\; =\; t\}\}\}$	REFL	рефлексивность равенства
$\Gamma \; ⊢\; s\; знак\; равно\; T\; \Delta \; ⊢\; T\; знак\; равно\; U\; \Gamma \; \cup \; \Delta \; ⊢\; s\; =\; u\; \{\backslash \; displaystyle\; \{\backslash \; cfrac\; \{\backslash \; Gamma\; \backslash \; vdash\; s\; =\; t\; \backslash \; qquad\; \backslash \; Delta\; \backslash \; vdash\; t\; =\; u\}\; \{\backslash \; Gamma\; \backslash \; cup\; \backslash \; Delta\; \backslash \; vdash\; s\; =\; u\}\}\}$	TRANS	транзитивность равенства
$\Gamma \; ⊢\; f\; =\; g\; \Delta \; ⊢\; x\; =\; y\; \Gamma \; \cup \; \Delta \; ⊢\; f\; (x)\; =\; g\; (y)\; \{\backslash \; displaystyle\; \{\; \backslash \; cfrac\; \{\backslash \; Gamma\; \backslash \; vdash\; f\; =\; g\; \backslash \; qquad\; \backslash \; Delta\; \backslash \; vdash\; x\; =\; y\}\; \{\backslash \; Gamma\; \backslash \; cup\; \backslash \; Delta\; \backslash \; vdash\; f\; (x)\; =\; g\; (y)\}\}\}$	MK_COMB	сравнение равенства
$\Gamma \; ⊢\; s\; =\; T\; \Gamma \; ⊢\; (\lambda \; x.\; s)\; =\; (\lambda \; x.\; t)\; \{\backslash \; displaystyle\; \{\backslash \; cfrac\; \{\backslash \; Gamma\; \backslash \; vdash\; s\; =\; t\}\; \{\backslash \; Gamma\; \backslash \; vdash\; (\backslash \; lambda\; xs)\; =\; (\backslash \; lambda\; xt)\}\}\}$	ABS	абстракция равенства ($x\; \{\backslash \; displaystyle\; x\}$не должна быть свободной в $\Gamma \; \{\; \backslash \; displaystyle\; \backslash \; Gamma\}$)
$⊢\; (\lambda \; x.\; t)\; x\; =\; t\; \{\backslash \; displaystyle\; \{\backslash \; cfrac\; \{\backslash \; qquad\}\; \{\backslash \; vdash\; (\backslash \; lambda\; xt)\; x\; =\; t\}\}\}$	БЕТА	соединение абстракции и приложения функции
$\{p\}\; ⊢\; p\; \{\backslash \; displaystyle\; \{\backslash \; cfrac\; \{\backslash \; qquad\}\; \{\backslash \; \{p\; \backslash \; \}\; \backslash \; vdash\; p\}\}\}$	ПРИНЯТЬ	предполагая $p\; \{\backslash \; displaystyle\; p\}$, доказать $p\; \{\backslash \; displaystyle\; p\}$
$\Gamma \; ⊢\; p\; знак\; равно\; q\; \Delta \; ⊢\; п\; \Gamma \; \cup \; \Delta \; ⊢\; q\; \{\backslash \; displaystyle\; \{\backslash \; cfrac\; \{\backslash \; Gamma\; \backslash \; vdash\; p\; =\; q\; \backslash \; qquad\; \backslash \; Delta\; \backslash \; vdash\; p\}\; \{\backslash \; Gamma\; \backslash \; cup\; \backslash \; Delta\; \backslash \; vdash\; q\}\}\}$	EQ_MP	отношение равенства и дедукции
$\Gamma \; ⊢\; p\; \Delta \; ⊢\; q\; (\Gamma \; -\; \{q\})\; \cup \; (\Delta \; -\; \{p\})\; ⊢\; p\; =\; q\; \{\backslash \; displaystyle\; \{\backslash \; cfrac\; \{\backslash \; Gamma\; \backslash \; vdash\; p\; \backslash \; qquad\; \backslash \; Delta\; \backslash \; vdash\; q\}\; \{(\backslash \; Gamma\; -\; \backslash \; \{q\; \backslash \})\; \backslash \; cup\; (\backslash \; Delta\; -\; \backslash \; \{p\; \backslash \})\; \backslash \; vdash\; p\; =\; q\}\}\}$	DEDUCT_ANTISYM_RULE	вывести равенство из 2-сторонней выводимости
$\Gamma \; [x\; 1,\dots ,\; xn]\; ⊢\; p\; [x\; 1,\dots ,\; xn]\; \Gamma \; [t\; 1,\dots ,\; tn]\; ⊢\; p\; [t\; 1,\dots ,\; tn]\; \{\backslash \; displaystyle\; \{\backslash \; cfrac\; \{\backslash \; Gamma\; [x\_\; \{1\},\; \backslash \; ldots,\; x\_\; \{n\}]\; \backslash \; vdash\; p\; [x\_\; \{1\},\; \backslash \; ldots,\; x\_\; \{n\}]\}\; \{\backslash \; Gamma\; [t\_\; \{1\},\; \backslash \; ldots,\; t\_\; \{n\}]\; \backslash \; vdash\; p\; [t\_\; \{1\},\; \backslash \; ldots,\; t\_\; \{n\}]\}\}\}$	INST	экземпляры переменных в предположениях и заключении теоремы
$\Gamma \; [\alpha \; 1,\dots ,\; {\rm A}\; N]\; ⊢\; п\; [\alpha \; 1,\dots ,\; \alpha \; N]\; \Gamma \; [\tau \; 1,\dots ,\; \tau \; n]\; ⊢\; p\; [\tau \; 1,\dots ,\; \tau \; n]\; \{\backslash \; displaystyle\; \{\backslash \; cfrac\; \{\backslash \; Gamma\; [\backslash \; alpha\; \_\; \{1\},\; \backslash \; ldots,\; \backslash \; alpha\; \_\; \{n\}]\; \backslash \; vdash\; p\; [\backslash \; alpha\; \_\; \{1\},\; \backslash \; ldots,\; \backslash \; alpha\; \_\; \{n\}]\}\; \{\backslash \; Gamma\; [\backslash \; tau\; \_\; \{1\},\; \backslash \; ldots,\; \backslash \; tau\; \_\; \{n\}]\; \backslash \; vdash\; p\; [\backslash \; tau\; \_\; \{1\; \},\; \backslash \; ldots,\; \backslash \; tau\; \_\; \{n\}]\}\}\}$	INST_TYPE	экземпляры переменных типа в предположениях и заключении теоремы

Эта формулировка теории типов очень близка к описанной в раздел II.2 документа Lambek Scott (1986).

• Lambek, J ; Скотт, П.Дж. (1986), Введение в категориальную логику высшего порядка, Cambridge University Press, ISBN 9780521356534

• Freek Wiedijk (декабрь 2008 г.), «Формальное доказательство - начало работы» (PDF), Уведомления Американского математического общества, 55(11): 1408–1414, получено 14 декабря 2008 г.

• HOL Light