論理プログラミング
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/12/19 16:42 UTC 版)
特徴
論理と制御
論理プログラミングでは「ロジック（論理）＋コントロール（制御）＝アルゴリズム（算法）」とされている。ロジックとは、数理論理学の論理式を特定の解釈で投影したプログラム書式表現を指す。これの代表例はファクト（事実）とルール（規則）を列挙するものであり、ルールは論理包含を主体にする。コントロールとは、そのロジックに対して、一定のファクトまたは特定のゴール（目標）を起点にした任意の問題条件を与えて、一定の解決条件を導出（resolution）することを指す。これを問題解決と言う。ロジックとコントロールの融合は、多様な定理証明戦略を表現する[4]。
最も普及しているProlog系の論理プログラムで使われる導出原理は、論理式をこれ以上解消できない所まで変形させていく演繹や簡約である。そこでのロジックはホーン節で表現されており、コントロールにはSLD導出が使われている。
問題解決
問題解決（problem solving）とその実践の導出原理は、数理論理学の膨大な知識から様々なものが存在する。ここではシンプルなロジックの代表格のホーン節を例にする。ホーン節は最大1個の正リテラルを持つ選言標準形をベースにしており、命題論理のホーン節は、素直にAND-OR木に投影できる。（右図はこの説明には不向きだが、これしか無かったのであしからず）右図のAND-OR木では、最上ノードのPがゴールになり、末端ノードのT・U・R・Sはファクトになって、このように解釈できる。
if Q and R then P, if S then P, if T then Q, if U then Q.
それへの導出原理は、ファクトから問題解決する前向き連鎖と、ゴールから問題解決する後向き連鎖に大別される。前向き連鎖は、与えられたファクトから様々な別のファクトをゴールとして解答する演繹手法である。TとRを与えるとPが解答される。Sを与えるとPが解答される。前向き連鎖はエキスパートシステムなどに使われている。後向き連鎖は、与えられたゴールがファクトかどうかを解答する演繹手法である。Pを与えるとその前件のRおよびQのそのまた前件のTがファクトなのでPはファクトと解答される。後向き連鎖は論理型言語の代表Prologに使われている。
述語論理のホーン節は、AND-OR木の各ノードが命題から述語になるので複雑になる。各ノードの述語記号の項は、定項と変項に分かれるが、定項がファクトで、変項が単一化によるファクトに束縛可能なら、そのノードは述語から命題になれる。
失敗による否定
論理プログラムが節 H :- B1, ..., Bn から構成され、H, B1, ..., Bn が全てアトミックな述語論理式であれば、このプログラムは確定(definite)していると呼ばれ、ホーン節プログラムであるともいう。確定した論理プログラムの手続き的意味と宣言的意味は、そのまま述語論理的に解釈できる。否定を含めると、古典的論理との関係はそれほど直接的ではなくなる。「失敗による否定; negation-as-failure」推論規則によれば、ゴール Q がプログラムによって証明できない場合、その否定 not(Q) は証明されたと見なされる。これは古典的論理学では全く正しくない。公理から Q も not(Q) も導けない可能性がある。結果として、この規則は論理的例外と実用的困難さをもたらした。後方連鎖証明規則に「失敗による否定」を加えても完全ではない。その場合、プログラムを宣言的に読んで得られる論理的結果の全てを証明することができない。しかし、ほとんどの Prolog 系言語は「失敗による否定」を \+ という文字列を使って実装している。
完全ではないものの、プログラムとしての完全性（completion）という意味では「失敗による否定」規則は（ある制限下で）健全な推論規則であると言える。論理プログラムの完全性は Keith Clark が最初に定義した。おおまかに言えば、それはプログラム内の左辺に同じ述語のある全節の集合である。例えば、以下のようなものである:
H :- Body1.
....
H :- Bodyk.
これらは次の1つの論理式と等価である。
H iff (Body1 or ... or Bodyk)
ここで、iff は同値（if and only if）を意味する。完全性を主張するには、等号と等号に関する公理を明確にする必要もある。完全性は非単調推論のためのマッカーシーのサーカムスクリプションや閉世界仮説に密接に関連する。
知識表現
知識表現（knowledge representation）は、宣言的知識と手続き的知識に大別される。例えば「空から水」への知識は、宣言的では「雨」と表現され、そこから手続き的では「傘をさす」などと表現される。俗説になるが宣言的知識はintelligence、手続き的知識はwisdomとも言われる。Prologのホーン節と後向き連鎖のSLD導出と失敗による否定の非単調論理の論理プログラミングは、宣言的知識と手続き的知識の混合とされている。
- ^ Alain Colmerauer and Philippe Roussel, The birth of Prolog
- ^ Robert Kowalski. The Early Years of Logic Programming
- ^ Robert Kowalski. The Early Years of Logic Programming
- ^ R.A.Kowalski (July 1979). “Algorithm=Logic + Control”. Communications of the ACM 22 (7): 424–436. doi:10.1145/359131.359136.
- ^ Kenneth Kahn, and Viyaj Saraswat, Actors as a Special Case of Concurrent Constraint Programming
論理プログラミングと同じ種類の言葉
- 論理プログラミングのページへのリンク
