ホーン節
ヒルベルトの時代から命題論理と第一階述語論理の任意の普遍妥当な論理式は、公理と推論規則をうまく定めれば機械的にすべて導出することができることは判明していたがその効率は非常に悪かった。エルブランの定理の改良として1965年にロビンソンが導出原理(resolution principle)にもとづく導出法(resolution)を提案した。Kowalski は「Predicate Logic as Programming Language」の中で論理式をプログラムと見る立場を明確に述べ、その際に改めて論理プログラミングの世界に導入された中心的概念がホーン節(Horn clause)である。
ホーン節は論理プログラミングの基本であり、プログラミング言語の Prolog, GHC のコードは表記として第二形式のホーン節そのものである。
ホーン節は計算複雑性理論にも関連する。ホーン節の論理積が真となるような各変数の値の組合せを探す問題はP完全問題であり、ホーン充足可能性問題(HORNSAT)とも呼ばれる。これはNP完全問題の1つである充足可能性問題のサブセットである。