「論理プログラミング」の版間の差分

削除された内容追加された内容

インライン

2022年6月10日 (金) 22:00時点における最新版

論理プログラミング（Logic Programming）とは、数理論理学（記号論理学）を基礎にしたプログラミングパラダイム、または数理論理学のコンピュータプログラミングへの応用である。形式論理の論理式をソースコードの書式に投影することが基本になる。プログラミングに適用するための幅広い解釈が加えられており、研究対象としての論理プログラミングは非常に多様である。

より一般的に受け入れられている論理プログラミングは、述語論理を基礎にし、問題領域の事実と規則を論理式モデル書式で表現して（ロジック）非決定性の演繹の導出原理を用いる（コントロール）というものである。このアルゴリズムスタイルで最も普及した論理プログラミング言語は「Prolog」である。

概要

論理プログラミングの基本は数理論理学のスタイルをコンピュータのプログラミングに持ち込むことにある。数学者や哲学者は論理を理論構築のツールとして選んだ。多くの問題は理論として自然に表現される。解決すべき問題とは、新たな仮説が既存の理論で説明できるかどうかを問うことと等しい。論理は問題が真か偽かを証明する方法を提供する。証明構築過程は明確であり、論理は問題に答える信頼できる方法と見なされている。論理プログラミングシステムはこの過程を自動化する。人工知能は論理プログラミングの開発に重要な影響を与えた。

この観点での論理プログラミングは、ジョン・マッカーシー[1958]のadvice takerの提案にまでさかのぼることができる。より一般的に受け入られている狭い意味での論理プログラミングは、述語論理式を非決定的なプログラミング言語とみなすもので、述語論理式は宣言的であると同時に手続き的にも解釈される。

論理をベースにしたプログラミング言語として1971年に Planner のサブセットである Micro-Planner が開発された。表明とゴールからパターンによる手続き的計画を呼び出す機能を備えていたが、十分に形式化されていなかった^[1]。Plannerと独立してより論理を重視した Prolog が開発され、コワルスキーにより述語論理式(ホーン節)のプログラム的解釈の考え方と結び付き、論理プログラミングの基本的な考え方が確立した^[2]。Planner からの派生で、プログラミング言語 Poplerが開発された。Prolog からの派生言語としては、Mercury、Visual Prolog、Oz、Fril などがある。バックトラッキングを使用しない並行論理プログラミング言語としてProlog からの派生したConcurrent Prolog、PARLOG、GHC、KL1などの各種言語（Shapiro [1989] に調査結果がある）がある。

数理論理学適用の限界

ジョン・マッカーシーは数理論理学をコンピュータシステムの認識論の基礎として利用することを提案した。MITではマービン・ミンスキーとシーモア・パパートが主導して、マッカーシーとは異なる手続き的手法が開発された。Planner が開発されたとき、これら2つの手法の関係に関する疑問が生まれた。Robert Kowalski は「計算は推論に包含される」という命題を生み出した。彼はこれを 1988年の Pat Hayes の論文にあった言葉「計算は制御された推論である」が元になっているとしている。Kowalski や Hayes とは逆に、カール・ヒューイットは「論理的推論はオープンシステムの並行計算を実行することが不可能だ」という命題を生み出した。

論理的手法と手続き的手法の関係という問題の答えは、手続き的手法の数学的意味（表示的意味論）と論理の数学的意味（モデル理論）は異なる、ということである。

歴史

論理プログラミングは、1950年代から盛んになった自動定理証明と、1958年公開言語「LISP」を最初の実践手段にしている。マサチューセッツ工科大学でLISPを開発したジョン・マッカーシーは、Advice taker（英語版）という常識推論仮説を発表している。

適切な形式言語（述語論理計算の一部に近い）を処理するプログラムは共通の”声明書”になる。基本プログラムは前提から直ちに結論を導き出す。その結論は宣言的かもしれないし命令的かもしれない。命令的結論が導出されたら、プログラムはそれに応じた動作もする。

ジョン・マッカーシーは更にこう補足しており、これは最初の人工知能仮説のようである。

我々がadvice takerに期待する主な利点は、その記号環境と探求物についての”声明”を作成するだけで、その動作が改良されるということである。”声明”の作成には、プログラム知識やadvice takerの事前知識をほとんど要求されないだろう。advice takerは事前知識に基づく広範囲な論理的帰結を取り揃えられると仮定できる。従って次のように言える。『事前知識を豊富に与えられ、自動演繹を行うプログラムは常識を備えている』

なお、マッカーシーは現代で言われる論理プログラミングの形態にはそれほど関与していない。

宣言的知識表現と手続き的知識表現

1965年頃、スタンフォード大学のコーデル・グリーン（英語版）が、節形式（clausal form）のプログラムとその導出原理を考案した。これはジョン・アラン・ロビンソン（英語版）の命題論理の単一化の演繹法を参考にしていた。1967年にアバディーン大学で開発された言語「Absys（英語版）」は最初期の論理プログラミングとして知られている。

1960年代の論理プログラミングの進展を通して、数理論理学に忠実な宣言的知識表現と、最適化アルゴリズムを取り入れる手続き的知識表現のどちらを指針にするべきかという議題が提起されていた。宣言的の支持者は、スタンフォード大学とエディンバラ大学中心のジョン・アラン・ロビンソン（英語版）、コーデル・グリーン（英語版）、バートラム・ラファエル（英語版）、パット・ヘイズ（英語版）、ロバート・コワルスキ（英語版）らであった。手続き的の支持者は、マサチューセッツ工科大学中心のマービン・ミンスキー、シーモア・パパート、カール・ヒューイット、ジェラルド・サスマン、テリー・ウィノグラード、ユージン・チャニアク（英語版）らであった。

Plannerの登場

1969年、カール・ヒューイット設計の論理型言語「Planner」がマサチューセッツ工科大学で開発された。メインフレーム前提のPlannerの大規模さは運用できる環境を制限したので、1971年にポータビリティ重視のサブセット版「Micro-Planner」が、ジェラルド・サスマンとテリー・ウィノグラードらによって開発された。

1971年、パパート、サスマン、チャニアクらのMIT勢が、エディンバラ大学を訪問してMicro-PlannerとSHRDLUを披露した。当時の同大学は、対話型自動定理証明プロジェクト「Logic for computable functions」が始動されていた論理プログラミングのメッカであった。Micro-Plannerなどを見たパット・ヘイズ（英語版）らは手続き的の価値を認め、同大学でもMicro-Plannerのサブセット版を実装してその有用性を確認した。Plannerを研究したロバート・コワルスキ（英語版）は、アルフレッド・ホーン発案のホーン節の論理プログラミング導入を提唱し、それへのSLD導出を考案している。更にエディンバラ大学ではPlannerのスーパーセット版「Popler」も開発された。

Prologの登場

1972年、マルセイユ大学のアラン・カルメラウアー（英語版）らは、コワルスキらの助言を得てホーン節とSLD導出をベースにした論理型言語「Prolog」を開発した。Prologに対する意見は分かれ、カール・ヒューイットなどはMicro-Plannerの複製品であると言い、コワルスキは論理プログラミングへの良いアプローチであると評した^[2]。カルメラウアーの元祖版は「Marseille Prolog」と呼ばれる。コワルスキの門弟デビッド・ウォーレン（英語版）のエディンバラ大学開発版は「Edinburgh Prolog」と呼ばれ、その系譜の1977年開発版「DEC-10 Prolog」がPrologの標準形になった。1979年にコワルスキはインペリアル・カレッジ・ロンドンで論理プログラミング基礎大全『Logic for Problem Solving』を上梓した。

1983年、ウォーレンはSRIインターナショナルでProlog言語処理系標準モデルのウォーレン抽象マシン（英語版）を策定し、Prologの普及に努めた。1986年に論理プログラミング協会（英語版）が設立された。1987年にDEC-10系譜の「SWI-Prolog（英語版）」がアムステルダム大学のジャン・ウィールメーカー（英語版）によって開発され、これが現在最も使われているPrologになっている。

1980年代の日本の情報工学分野ではProlog研究が盛んに行われており、人工知能コンピュータ開発を目的にした第五世代コンピュータ計画の中心になっていた。

特徴

論理と制御

論理プログラミングでは「ロジック（論理）＋コントロール（制御）＝アルゴリズム（算法）」とされている。ロジックとは、数理論理学の論理式を特定の解釈で投影したプログラム書式表現を指す。これの代表例はファクト（事実）とルール（規則）を列挙するものであり、ルールは論理包含を主体にする。コントロールとは、そのロジックに対して、一定のファクトまたは特定のゴール（目標）を起点にした任意の問題条件を与えて、一定の解決条件を導出（resolution）することを指す。これを問題解決と言う。ロジックとコントロールの融合は、多様な定理証明戦略を表現する^[3]。

最も普及している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 :- B₁, ..., B_n から構成され、H, B₁, ..., B_n が全てアトミックな述語論理式であれば、このプログラムは確定(definite)していると呼ばれ、ホーン節プログラムであるともいう。確定した論理プログラムの手続き的意味と宣言的意味は、そのまま述語論理的に解釈できる。否定を含めると、古典的論理との関係はそれほど直接的ではなくなる。「失敗による否定; negation-as-failure」推論規則によれば、ゴール Q がプログラムによって証明できない場合、その否定 not(Q) は証明されたと見なされる。これは古典的論理学では全く正しくない。公理から Q も not(Q) も導けない可能性がある。結果として、この規則は論理的例外と実用的困難さをもたらした。後方連鎖証明規則に「失敗による否定」を加えても完全ではない。その場合、プログラムを宣言的に読んで得られる論理的結果の全てを証明することができない。しかし、ほとんどの Prolog 系言語は「失敗による否定」を \+ という文字列を使って実装している。

完全ではないものの、プログラムとしての完全性（completion）という意味では「失敗による否定」規則は（ある制限下で）健全な推論規則であると言える。論理プログラムの完全性は Keith Clark が最初に定義した。おおまかに言えば、それはプログラム内の左辺に同じ述語のある全節の集合である。例えば、以下のようなものである:

     H :-  Body₁.
     ....
     H :-  Body_k.

これらは次の1つの論理式と等価である。

     H iff (Body₁ or ... or Body_k)

ここで、iff は同値（if and only if）を意味する。完全性を主張するには、等号と等号に関する公理を明確にする必要もある。完全性は非単調推論のためのマッカーシーのサーカムスクリプションや閉世界仮説に密接に関連する。

知識表現

知識表現（knowledge representation）は、宣言的知識と手続き的知識に大別される。例えば「空から水」への知識は、宣言的では「雨」と表現され、そこから手続き的では「傘をさす」などと表現される。俗説になるが宣言的知識はintelligence、手続き的知識はwisdomとも言われる。Prologのホーン節と後向き連鎖のSLD導出と失敗による否定の非単調論理の論理プログラミングは、宣言的知識と手続き的知識の混合とされている。

Prolog

→詳細は「Prolog」を参照

Prolog は 1972年にマルセイユのカルメラウアーが考案し、1974年にコワルスキーがさらに形式的に定義し、数理論理学に基づいた言語として発表した。Prolog のプログラムは一階述語論理のサブセットの論理式の集まりとして読むことができ、一階述語論理のモデル理論と証明理論を継承している。プログラムの節は次のように書かれる:

   H :-  B₁, ..., B_n.

これを宣言として読めば、以下の論理的含意に等しい：

   B₁ and ... and B_n implies H

ここで、節内の全変数（変項）は全称量化されている。手続き的な後方連鎖規則として見れば、H を証明するには、B₁ から B_n までを証明できれば十分であることがわかる。手続き的意味は線形導出法（LUSH または SLD導出法）による反駁証明によっても定式化できる。宣言的意味と手続き的意味の密接な関係は論理プログラミング言語の際立った特徴であるが、否定や論理和といった他の量化子をプログラム内に許すようになると関係は複雑になる。

Prolog の実装

最初に実装された Prolog処理系は1972年に開発された Marseille Prolog である。Prolog が実用的なプログラミング言語として使われるきっかけとなったのは 1977年にエジンバラで David Warren がコンパイラ処理系を開発したことであった。Edinburgh Prolog は他の記号処理言語（Lispなど）と処理速度を比較して遜色ない性能であることを世に示した。Edinburgh Prolog はデファクトスタンダードとなり、後の ISO での Prolog 標準化に影響を与えた。

派生分野

並行論理プログラミング

→詳細は「並行論理プログラミング」を参照

Keith Clark、Hervé Gallaire、Steve Gregory、Vijay Saraswat、Udi Shapiro、Kazunori Ueda（上田和紀）らは、共有変数のユニフィケーション機能とメッセージのためのデータ構造ストリーム機能を備えた並行論理プログラミング言語を開発した。数理論理学に基づく並行プログラミングの基礎を築くための研究であるが、これが第五世代コンピュータの基盤ともなった。

並行論理プログラミングは制約論理プログラミングと結び付き、制約で並行実行を制御する並行制約プログラミングとして統合され、 Saraswatらにより理論化が行われた。KahnとSaraswatは並行制約プログラミングの枠内での制約の設定でアクターモデルが実現できることから、アクターモデルは並行制約プログラミングの特別なケースだと主張した^[4]。

Concurrent Prolog、PARLOG、GHC、KL1
Oz、Alice（英語版）、ToonTalk（英語版）

制約論理プログラミング

→詳細は「制約論理プログラミング」を参照

述語記号の項に、制約（英語版）も含めるようにしている。制約（constraint）とは値（元・要素・個体）を”関係性”で表現したものであり、決定変数の集合で定義される計算対象である。

B-Prolog（英語版）、Ciao（英語版）、ECLiPSe（英語版）、Fril（英語版）

高階論理プログラミング

述語記号の項に、述語記号も含めるようにしている。例えば、p(A, B, C) :- q(A, foo), r(B, bar), C.では、Cを別個の述語記号にできる。テンプレートメタ的な書式も扱っており、例えばp(A, B, C) :- (C)(A, B)では、Cが述語名でAとBがその項になる。

λProlog（英語版）、HiLog（英語版）

関数論理プログラミング

述語記号と関数記号の双方をリテラルにしている。

Mercury（英語版）、Curry（英語版）

オブジェクト指向論理プログラミング

ファクトとルールをまとめたモジュールを扱っている。module.predicate(A, B, C)のように表記できる。モジュールは、オブジェクト指向由来の継承と多態性を備えている。既存の上位モジュールを継承して新規の下位モジュールを定義できる。上位モジュールの変数に下位モジュールを代入してサブタイピングするのが多態性である。例えばvar.predicate(A, B, C)では、上位変数varに下位モジュールAを代入するとAのpredicateと解釈され、同変数に下位モジュールBを代入するとBのpredicateと解釈される。

Visual Prolog（英語版）

線形論理プログラミング

線形論理を扱っている。

帰納論理プログラミング

帰納推論を扱っている。これまでの演繹推論とは別種になる。

仮説論理プログラミング

仮説推論を扱っている。これまでの演繹推論とは別種になる。

適用分野

エキスパートシステム: 特定応用分野の巨大なモデルから、推奨や回答を生成するプログラム
自動定理証明: 既存の理論から新たな定理を生成するプログラム

脚注

[脚注の使い方]

^ Alain Colmerauer and Philippe Roussel, The birth of Prolog
^ ^a ^b 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

参考文献

Alain Colmerauer and Philippe Roussel, ’The birth of Prolog', in The second ACM SIGPLAN conference on History of programming languages, p. 37-52, 1992.
John McCarthy. Programs with common sense Symposium on Mechanization of Thought Processes. National Physical Laboratory. Teddington, England. 1958.
Fisher Black. A deductive question answering system Harvard University. Thesis. 1964.
James Slagle. Experiments with a Deductive Question-Answering Program CACM. December, 1965.
Cordell Green. Application of Theorem Proving to Problem Solving IJCAI 1969.
Carl Hewitt. Planner: A Language for Proving Theorems in Robots IJCAI 1969.
Gerry Sussman and Terry Winograd. Micro-planner Reference Manual AI Memo No, 203, MIT Project MAC, July 1970.
Carl Hewitt. Procedural Embedding of Knowledge In Planner IJCAI 1971.
Terry Winograd. Procedures as a Representation for Data in a Computer Program for Understanding Natural Language MIT AI TR-235. January 1971.
Bruce Anderson. Documentation for LIB PICO-PLANNER School of Artificial Intelligence, Edinburgh University. 1972
Bruce Baumgart. Micro-Planner Alternate Reference Manual Stanford AI Lab Operating Note No. 67, April 1972.
Julian Davies. Popler 1.6 Reference Manual University of Edinburgh, TPU Report No. 1, May 1973.
Jeff Rulifson, Jan Derksen, and Richard Waldinger. QA4, A Procedural Calculus for Intuitive Reasoning SRI AI Center Technical Note 73, November 1973.
Robert Kowalski Predicate Logic as a Programming Language Memo 70, Department of Artificial Intelligence, Edinburgh University. 1973.
Drew McDermott and Gerry Sussman. The Conniver Reference Manual MIT AI Memo 259A. January 1974.
Earl Sacerdoti, et al. QLISP: A Language for the Interactive Development of Complex Systems AFIPS National Computer Conference. 1976.
Bill Kornfeld and Carl Hewitt. The Scientific Community Metaphor IEEE Transactions on Systems, Man, and Cybernetics. January 1981.
Bill Kornfeld. The Use of Parallelism to Implement a Heuristic Search IJCAI 1981.
Bill Kornfeld. Parallelism in Problem Solving MIT EECS Doctoral Dissertation. August 1981.
Bill Kornfeld. Combinatorially Implosive Algorithms CACM. 1982
Carl Hewitt. The Challenge of Open Systems Byte Magazine. April 1985.
Robert Kowalski. The limitation of logic Proceedings of the 1986 ACM fourteenth annual conference on Computer science.
Ehud Shapiro (Editor). Concurrent Prolog MIT Press. 1987.
Robert Kowalski. The Early Years of Logic Programming CACM. January 1988.
Ehud Shapiro. The family of concurrent logic programming languages ACM Computing Surveys. September 1989.
Carl Hewitt and Gul Agha. Guarded Horn clause languages: are they deductive and Logical? International Conference on Fifth Generation Computer Systems, Ohmsha 1988. Tokyo. Also in Artificial Intelligence at MIT, Vol. 2. MIT Press 1991.
Shunichi Uchida and Kazuhiro Fuchi Proceedings of the FGCS Project Evaluation Workshop Institute for New Generation Computer Technology (ICOT). 1992.
Carl Hewitt. The repeated demise of logic programming and why it will be reincarnated What Went Wrong and Why: Lessons from AI Research and Applications. Technical Report SS-06-08. AAAI Press. March 2006.
J. W. Lloyd. Foundations of Logic Programming (2nd edition). Springer-Verlag 1987.
Kenneth Kahn, and Viyaj Saraswat, Actors as a Special Case of Concurrent Constraint Programming, Xerox Technical Report, 1990.

外部リンク

[1] Alain Colmerauer and Philippe Roussel, The birth of Prolog

[#1-2] Robert Kowalski. The Early Years of Logic Programming

[3] R.A.Kowalski (July 1979). “Algorithm=Logic + Control”. Communications of the ACM 22 (7): 424–436. doi:10.1145/359131.359136.

[4] Kenneth Kahn, and Viyaj Saraswat, Actors as a Special Case of Concurrent Constraint Programming

[1]

[2]

[3]

[4]

@@ 1行目: / 1行目: @@
+{{プログラミング・パラダイム}}
-'''論理プログラミング'''（Logic Programming）とは、広い意味では、コンピュータプログラミングでの[[数理論理学]]の使用である。この観点での論理プログラミングは、[[ジョン・マッカーシー]][1958]の''advice taker''の提案にまでさかのぼることができる。
+'''論理プログラミング'''（Logic Programming）とは、[[数理論理学]]（記号論理学）を基礎にした[[プログラミングパラダイム]]、または[[数理論理学]]の[[コンピュータプログラミング]]への応用である。[[形式論理学|形式論理]]の[[論理式 (数学)|論理式]]を[[ソースコード]]の書式に投影することが基本になる。[[コンピュータプログラミング|プログラミング]]に適用するための幅広い解釈が加えられており、研究対象としての論理プログラミングは非常に多様である。
-より一般的に受け入られている狭い意味での論理プログラミングは、述語論理式を非決定的なプログラミング言語とみなすもので、述語論理式は宣言的であると同時に手続き的にも解釈される。
+より一般的に受け入れられている論理プログラミングは、[[述語論理]]を基礎にし、問題領域の事実と規則を論理式モデル書式で表現して（ロジック）[[非決定性チューリングマシン|非決定性]]の[[演繹]]の[[導出原理]]を用いる（コントロール）というものである。この[[アルゴリズム]]スタイルで最も普及した論理プログラミング言語は「[[Prolog]]」である。
-論理をベースにしたプログラミング言語として1971年に [[Planner]] のサブセットである Micro-Planner が開発された。表明とゴールからパターンによる手続き的計画を呼び出す機能を備えていたが、十分に形式化されていなかった<ref>Alain Colmerauer and Philippe Roussel, '''The birth of Prolog'''</ref>。Plannerと独立してより論理を重視した [[Prolog]] が開発され、コワルスキーにより述語論理式([[ホーン節]])のプログラム的解釈の考え方と結び付き、論理プログラミングの基本的な考え方が確立した<ref>Robert Kowalski. '''The Early Years of Logic Programming'''</ref>。
-Planner からの派生で、プログラミング言語 Poplerが開発された。Prolog からの派生言語としては、Mercury、Visual Prolog、[[Oz (プログラミング言語)|Oz]]、Fril などがある。バックトラッキングを使用しない[[並行論理プログラミング]]言語としてProlog からの派生した[[Concurrent Prolog]]、[[PARLOG]]、[[Guarded Horn Clauses|GHC]]、[[KL1]]などの各種言語（Shapiro [1989] に調査結果がある）がある。
+==概要==
-==数理論理学的基礎==
 論理プログラミングの基本は[[数理論理学]]のスタイルをコンピュータのプログラミングに持ち込むことにある。数学者や哲学者は論理を理論構築のツールとして選んだ。多くの問題は理論として自然に表現される。解決すべき問題とは、新たな仮説が既存の理論で説明できるかどうかを問うことと等しい。論理は問題が真か偽かを証明する方法を提供する。証明構築過程は明確であり、論理は問題に答える信頼できる方法と見なされている。論理プログラミングシステムはこの過程を自動化する。[[人工知能]]は論理プログラミングの開発に重要な影響を与えた。
+この観点での論理プログラミングは、[[ジョン・マッカーシー]][1958]の''advice taker''の提案にまでさかのぼることができる。より一般的に受け入られている狭い意味での論理プログラミングは、述語論理式を非決定的なプログラミング言語とみなすもので、述語論理式は宣言的であると同時に手続き的にも解釈される。
-==Prolog==
-{{ main|Prolog }}
+論理をベースにしたプログラミング言語として1971年に [[Planner]] のサブセットである Micro-Planner が開発された。表明とゴールからパターンによる手続き的計画を呼び出す機能を備えていたが、十分に形式化されていなかった<ref>Alain Colmerauer and Philippe Roussel, '''The birth of Prolog'''</ref>。Plannerと独立してより論理を重視した [[Prolog]] が開発され、コワルスキーにより述語論理式([[ホーン節]])のプログラム的解釈の考え方と結び付き、論理プログラミングの基本的な考え方が確立した<ref name="#1">Robert Kowalski. '''The Early Years of Logic Programming'''</ref>。Planner からの派生で、プログラミング言語 Poplerが開発された。Prolog からの派生言語としては、Mercury、Visual Prolog、[[Oz (プログラミング言語)|Oz]]、Fril などがある。バックトラッキングを使用しない[[並行論理プログラミング]]言語としてProlog からの派生した[[Concurrent Prolog]]、[[PARLOG]]、[[Guarded Horn Clauses|GHC]]、[[KL1]]などの各種言語（Shapiro [1989] に調査結果がある）がある。
-[[Prolog]] は 1972年にマルセイユのカルメラウアーが考案し、1974年にコワルスキーがさらに形式的に定義し、数理論理学に基づいた言語として発表した。Prolog のプログラムは[[一階述語論理]]のサブセットの論理式の集まりとして読むことができ、一階述語論理のモデル理論と証明理論を継承している。プログラムの節は次のように書かれる:
+'''数理論理学適用の限界'''
-    H :-  B<sub>1</sub>, ..., B<sub>n</sub>.
+ジョン・マッカーシーは数理論理学をコンピュータシステムの認識論の基礎として利用することを提案した。[[マサチューセッツ工科大学|MIT]]では[[マービン・ミンスキー]]と[[シーモア・パパート]]が主導して、マッカーシーとは異なる手続き的手法が開発された。[[Planner]] が開発されたとき、これら2つの手法の関係に関する疑問が生まれた。Robert Kowalski は「計算は推論に包含される」という命題を生み出した。彼はこれを 1988年の Pat Hayes の論文にあった言葉「計算は制御された推論である」が元になっているとしている。Kowalski や Hayes とは逆に、[[カール・ヒューイット]]は「論理的推論はオープンシステムの並行計算を実行することが不可能だ」という命題を生み出した。<!-- [[計算の不確定性]]参照 -->
-これを宣言として読めば、以下の論理的含意に等しい：
+論理的手法と手続き的手法の関係という問題の答えは、手続き的手法の数学的意味（[[表示的意味論]]）と論理の数学的意味（[[モデル理論]]）は異なる、ということである。
-    B<sub>1</sub> and ... and B<sub>n</sub> implies H
+==歴史==
-ここで、節内の全変数（変項）は[[全称記号|全称量化]]されている。手続き的な後方連鎖規則として見れば、<tt>H</tt> を証明するには、<tt>B<sub>1</sub></tt> から <tt>B<sub>n</sub></tt> までを証明できれば十分であることがわかる。手続き的意味は線形導出法（LUSH または SLD導出法）による反駁証明によっても定式化できる。宣言的意味と手続き的意味の密接な関係は論理プログラミング言語の際立った特徴であるが、否定や論理和といった他の量化子をプログラム内に許すようになると関係は複雑になる。
+論理プログラミングは、1950年代から盛んになった[[自動定理証明]]と、1958年公開言語「[[LISP]]」を最初の実践手段にしている。[[マサチューセッツ工科大学]]でLISPを開発した[[ジョン・マッカーシー]]は、{{仮リンク|Advice taker|en|Advice taker|label=}}という常識[[推論エンジン|推論]]仮説を発表している。
+{{quote|適切な形式言語（述語論理計算の一部に近い）を処理するプログラムは共通の”声明書”になる。基本プログラムは前提から直ちに結論を導き出す。その結論は宣言的かもしれないし命令的かもしれない。命令的結論が導出されたら、プログラムはそれに応じた動作もする。}}
-===論理プログラミングにおける否定===
+[[ジョン・マッカーシー]]は更にこう補足しており、これは最初の[[人工知能]]仮説のようである。
+{{quote|我々がadvice takerに期待する主な利点は、その記号環境と探求物についての”声明”を作成するだけで、その動作が改良されるということである。”声明”の作成には、プログラム知識やadvice takerの事前知識をほとんど要求されないだろう。advice takerは事前知識に基づく広範囲な論理的帰結を取り揃えられると仮定できる。従って次のように言える。『事前知識を豊富に与えられ、自動演繹を行うプログラムは常識を備えている』|}}
+なお、マッカーシーは現代で言われる論理プログラミングの形態にはそれほど関与していない。
+'''宣言的知識表現と手続き的知識表現'''
+年頃、[[スタンフォード大学]]の{{仮リンク|コーデル・グリーン|en|Cordell Green}}が、節形式（clausal form）のプログラムとその[[導出原理]]を考案した。これは{{仮リンク|ジョン・アラン・ロビンソン|en|John Alan Robinson}}の[[命題論理]]の[[単一化]]の[[演繹法]]を参考にしていた。1967年に[[アバディーン大学]]で開発された言語「{{仮リンク|Absys|en|Absys|label=}}」は最初期の論理プログラミングとして知られている。
+年代の論理プログラミングの進展を通して、[[数理論理学]]に忠実な[[宣言的知識|宣言的知識表現]]と、最適化アルゴリズムを取り入れる[[手続き的知識|手続き的知識表現]]のどちらを指針にするべきかという議題が提起されていた。宣言的の支持者は、[[スタンフォード大学]]と[[エディンバラ大学]]中心の{{仮リンク|ジョン・アラン・ロビンソン|en|John Alan Robinson}}、{{仮リンク|コーデル・グリーン|en|Cordell Green}}、{{仮リンク|バートラム・ラファエル|en|Bertram Raphael|label=}}、{{仮リンク|パット・ヘイズ|en|Pat Hayes|label=}}、{{仮リンク|ロバート・コワルスキ|en|Robert Kowalski|label=}}らであった。手続き的の支持者は、[[マサチューセッツ工科大学]]中心の[[マービン・ミンスキー]]、[[シーモア・パパート]]、[[カール・ヒューイット]]、[[ジェラルド・ジェイ・サスマン|ジェラルド・サスマン]]、[[テリー・ウィノグラード]]、{{仮リンク|ユージン・チャニアク|en|Eugene Charniak|label=}}らであった。
+'''Plannerの登場'''
+年、[[カール・ヒューイット]]設計の論理型言語「[[Planner]]」が[[マサチューセッツ工科大学]]で開発された。[[メインフレーム]]前提のPlannerの大規模さは運用できる環境を制限したので、1971年に[[ポータビリティ]]重視のサブセット版「Micro-Planner」が、[[ジェラルド・ジェイ・サスマン|ジェラルド・サスマン]]と[[テリー・ウィノグラード]]らによって開発された。
+年、パパート、サスマン、チャニアクらの[[MIT]]勢が、[[エディンバラ大学]]を訪問してMicro-Plannerと[[SHRDLU]]を披露した。当時の同大学は、対話型[[自動定理証明]]プロジェクト「Logic for computable functions」が始動されていた論理プログラミングのメッカであった。Micro-Plannerなどを見た{{仮リンク|パット・ヘイズ|en|Pat Hayes|label=}}らは[[手続き的知識|手続き的]]の価値を認め、同大学でもMicro-Plannerのサブセット版を実装してその有用性を確認した。Plannerを研究した{{仮リンク|ロバート・コワルスキ|en|Robert Kowalski|label=}}は、[[アルフレッド・ホーン]]発案の[[ホーン節]]の論理プログラミング導入を提唱し、それへのSLD導出を考案している。更にエディンバラ大学ではPlannerのスーパーセット版「Popler」も開発された。
+'''Prologの登場'''
+年、[[マルセイユ大学]]の{{仮リンク|アラン・カルメラウアー|en|Alain Colmerauer|label=}}らは、{{仮リンク|コワルスキ|en|Robert Kowalski|label=}}らの助言を得て[[ホーン節]]とSLD導出をベースにした論理型言語「[[Prolog]]」を開発した。Prologに対する意見は分かれ、[[カール・ヒューイット]]などはMicro-Plannerの複製品であると言い、コワルスキは論理プログラミングへの良いアプローチであると評した<ref name="#1"/>。カルメラウアーの元祖版は「Marseille Prolog」と呼ばれる。コワルスキの門弟{{仮リンク|デビッド・ウォーレン|en|David H. D. Warren|label=}}の[[エディンバラ大学]]開発版は「Edinburgh Prolog」と呼ばれ、その系譜の1977年開発版「DEC-10 Prolog」がPrologの標準形になった。1979年にコワルスキは[[インペリアル・カレッジ・ロンドン]]で論理プログラミング基礎大全『''Logic for Problem Solving''』を上梓した。
+年、ウォーレンは[[SRIインターナショナル]]でProlog言語処理系標準モデルの{{仮リンク|ウォーレン抽象マシン|en|Warren Abstract Machine|label=}}を策定し、Prologの普及に努めた。1986年に{{仮リンク|論理プログラミング協会|en|Association for Logic Programming|label=}}が設立された。1987年にDEC-10系譜の「{{仮リンク|SWI-Prolog|en|SWI-Prolog|label=}}」が[[アムステルダム大学]]の{{仮リンク|ジャン・ウィールメーカー|en|Jan Wielemaker|label=}}によって開発され、これが現在最も使われているPrologになっている。
+年代の日本の[[情報工学]]分野では[[Prolog]]研究が盛んに行われており、人工知能コンピュータ開発を目的にした[[第五世代コンピュータ]]計画の中心になっていた。
+== 特徴 ==
+=== 論理と制御 ===
+論理プログラミングでは「ロジック（論理）＋コントロール（制御）＝アルゴリズム（算法）」とされている。ロジックとは、[[数理論理学]]の[[論理式 (数学)|論理式]]を特定の解釈で投影したプログラム書式表現を指す。これの代表例はファクト（事実）とルール（規則）を列挙するものであり、ルールは[[論理包含]]を主体にする。コントロールとは、そのロジックに対して、一定のファクトまたは特定のゴール（目標）を起点にした任意の問題条件を与えて、一定の解決条件を導出（resolution）することを指す。これを問題解決と言う。ロジックとコントロールの融合は、多様な[[自動定理証明|定理証明]]戦略を表現する<ref>{{cite journal|author=R.A.Kowalski|date=July 1979|title=Algorithm=Logic + Control|journal=Communications of the ACM|volume=22|issue=7|pages=424–436|doi=10.1145/359131.359136|s2cid=2509896}}</ref>。
+最も普及している[[Prolog]]系の論理プログラムで使われる[[導出原理]]は、[[論理式 (数学)|論理式]]をこれ以上解消できない所まで変形させていく[[演繹]]や簡約である。そこでのロジックは[[ホーン節]]で表現されており、コントロールにはSLD導出が使われている。
+=== 問題解決 ===
+[[ファイル:Andortree.png|サムネイル|200x200ピクセル|and-or木]]
+問題解決（problem solving）とその実践の[[導出原理]]は、[[数理論理学]]の膨大な知識から様々なものが存在する。ここではシンプルなロジックの代表格の[[ホーン節]]を例にする。[[ホーン節]]は最大1個の正リテラルを持つ[[選言標準形]]をベースにしており、[[命題論理]]のホーン節は、素直に{{仮リンク|AND-OR木|en|And-or tree|label=}}に投影できる。（右図はこの説明には不向きだが、これしか無かったのであしからず）右図のAND-OR木では、最上ノードのPがゴールになり、末端ノードのT・U・R・Sはファクトになって、このように解釈できる。
+<code>if Q and R then P</code>,  <code>if S then P</code>,  <code>if T then Q</code>,  <code>if U then Q</code>.
+それへの[[導出原理]]は、ファクトから問題解決する[[前向き連鎖]]と、ゴールから問題解決する[[後向き連鎖]]に大別される。前向き連鎖は、与えられたファクトから様々な別のファクトをゴールとして解答する演繹手法である。TとRを与えるとPが解答される。Sを与えるとPが解答される。前向き連鎖は[[エキスパートシステム]]などに使われている。後向き連鎖は、与えられたゴールがファクトかどうかを解答する演繹手法である。Pを与えるとその前件のRおよびQのそのまた前件のTがファクトなのでPはファクトと解答される。後向き連鎖は論理型言語の代表[[Prolog]]に使われている。
+[[述語論理]]の[[ホーン節]]は、AND-OR木の各ノードが命題から述語になるので複雑になる。各ノードの述語記号の項は、定項と[[変項]]に分かれるが、定項がファクトで、変項が[[単一化]]によるファクトに束縛可能なら、そのノードは述語から命題になれる。
+=== 失敗による否定 ===
 論理プログラムが節 H :- B<sub>1</sub>, ..., B<sub>n</sub> から構成され、H, B<sub>1</sub>, ..., B<sub>n</sub> が全てアトミックな述語論理式であれば、このプログラムは確定(definite)していると呼ばれ、[[ホーン節]]プログラムであるともいう。確定した論理プログラムの手続き的意味と宣言的意味は、そのまま述語論理的に解釈できる。否定を含めると、古典的論理との関係はそれほど直接的ではなくなる。「[[失敗による否定]]; negation-as-failure」推論規則によれば、ゴール Q がプログラムによって証明できない場合、その否定 not(Q) は証明されたと見なされる。これは古典的論理学では全く正しくない。公理から Q も not(Q) も導けない可能性がある。結果として、この規則は論理的例外と実用的困難さをもたらした。後方連鎖証明規則に「失敗による否定」を加えても完全ではない。その場合、プログラムを宣言的に読んで得られる論理的結果の全てを証明することができない。しかし、ほとんどの Prolog 系言語は「失敗による否定」を '''\+''' という文字列を使って実装している。
@@ 36行目: / 80行目: @@
 ここで、''iff'' は[[同値]]（if and only if）を意味する。完全性を主張するには、等号と等号に関する公理を明確にする必要もある。完全性は非単調推論のためのマッカーシーの[[サーカムスクリプション]]や[[閉世界仮説]]に密接に関連する。
-===Prolog の実装===
+=== 知識表現 ===
+知識表現（knowledge representation）は、[[宣言的知識]]と[[手続き的知識]]に大別される。例えば「空から水」への知識は、宣言的では「雨」と表現され、そこから手続き的では「傘をさす」などと表現される。俗説になるが宣言的知識はintelligence、手続き的知識はwisdomとも言われる。[[Prolog]]の[[ホーン節]]と[[後向き連鎖]]のSLD導出と[[失敗による否定]]の[[非単調論理]]の論理プログラミングは、宣言的知識と手続き的知識の混合とされている。
-最初に実装された [[Prolog]]処理系は1972年に開発された Marseille Prolog である。Prolog が実用的なプログラミング言語として使われるきっかけとなったのは 1977年にエジンバラで David Warren がコンパイラ処理系を開発したことであった。Edinburgh Prolog は他の記号処理言語（Lispなど）と処理速度を比較して遜色ない性能であることを世に示した。Edinburgh Prolog はデファクトスタンダードとなり、後の ISO での Prolog 標準化に影響を与えた。
+==Prolog==
-==数理論理学のプログラミングへの利用の限界==
+{{ main|Prolog }}
-ジョン・マッカーシーは数理論理学をコンピュータシステムの認識論の基礎として利用することを提案した。[[マサチューセッツ工科大学|MIT]]では[[マービン・ミンスキー]]と[[シーモア・パパート]]が主導して、マッカーシーとは異なる手続き的手法が開発された。[[Planner]] が開発されたとき、これら2つの手法の関係に関する疑問が生まれた。Robert Kowalski は「計算は推論に包含される」という命題を生み出した。彼はこれを 1988年の Pat Hayes の論文にあった言葉「計算は制御された推論である」が元になっているとしている。Kowalski や Hayes とは逆に、[[カール・ヒューイット]]は「論理的推論はオープンシステムの並行計算を実行することが不可能だ」という命題を生み出した。<!-- [[計算の不確定性]]参照 -->
+[[Prolog]] は 1972年にマルセイユのカルメラウアーが考案し、1974年にコワルスキーがさらに形式的に定義し、数理論理学に基づいた言語として発表した。Prolog のプログラムは[[一階述語論理]]のサブセットの論理式の集まりとして読むことができ、一階述語論理のモデル理論と証明理論を継承している。プログラムの節は次のように書かれる:
+    H :-  B<sub>1</sub>, ..., B<sub>n</sub>.
-論理的手法と手続き的手法の関係という問題の答えは、手続き的手法の数学的意味（[[表示的意味論]]）と論理の数学的意味（[[モデル理論]]）は異なる、ということである。
+これを宣言として読めば、以下の論理的含意に等しい：
+    B<sub>1</sub> and ... and B<sub>n</sub> implies H
+ここで、節内の全変数（変項）は[[全称記号|全称量化]]されている。手続き的な後方連鎖規則として見れば、<tt>H</tt> を証明するには、<tt>B<sub>1</sub></tt> から <tt>B<sub>n</sub></tt> までを証明できれば十分であることがわかる。手続き的意味は線形導出法（LUSH または SLD導出法）による反駁証明によっても定式化できる。宣言的意味と手続き的意味の密接な関係は論理プログラミング言語の際立った特徴であるが、否定や論理和といった他の量化子をプログラム内に許すようになると関係は複雑になる。
+'''Prolog の実装'''
+最初に実装された [[Prolog]]処理系は1972年に開発された Marseille Prolog である。Prolog が実用的なプログラミング言語として使われるきっかけとなったのは 1977年にエジンバラで David Warren がコンパイラ処理系を開発したことであった。Edinburgh Prolog は他の記号処理言語（Lispなど）と処理速度を比較して遜色ない性能であることを世に示した。Edinburgh Prolog はデファクトスタンダードとなり、後の ISO での Prolog 標準化に影響を与えた。
+== 派生分野 ==
-==並行論理プログラミング==
+===並行論理プログラミング===
 {{ main|並行論理プログラミング }}
@@ 51行目: / 108行目: @@
 並行論理プログラミングは[[制約論理プログラミング]]と結び付き、制約で並行実行を制御する[[並行制約プログラミング]]として統合され、 Saraswatらにより理論化が行われた。KahnとSaraswatは並行制約プログラミングの枠内での制約の設定で[[アクターモデル]]が実現できることから、アクターモデルは並行制約プログラミングの特別なケースだと主張した<ref>Kenneth Kahn, and Viyaj Saraswat, '''Actors as a Special Case of Concurrent Constraint Programming'''</ref>。
+* [[Concurrent Prolog]]、[[PARLOG]]、[[Guarded Horn Clauses|GHC]]、[[KL1]]
-==高階論理プログラミング==
+* [[Oz (プログラミング言語)|Oz]]、{{仮リンク|アリス言語|en|Alice (programming language)|label=Alice}}、{{仮リンク|ToonTalk|en|ToonTalk|label=}}
-一部の研究者は[[高階述語論理]]に基づいた高階論理プログラミングへと拡張を行った（述語の変項化など）。そのような言語としては Prolog の拡張である HiLog や {{仮リンク|λProlog|en|ΛProlog}}がある。
+=== 制約論理プログラミング ===
+{{main|制約論理プログラミング}}述語記号の項に、{{仮リンク|制約（数学）|en|Constraint (mathematics)|label=制約}}も含めるようにしている。制約（constraint）とは値（元・要素・個体）を”関係性”で表現したものであり、決定変数の集合で定義される計算対象である。
+* {{仮リンク|B-Prolog|en|B-Prolog|label=}}、{{仮リンク|Ciao言語|en|Ciao (programming language)|label=Ciao}}、{{仮リンク|ECLiPSe|en|ECLiPSe|label=}}、{{仮リンク|Fril|en|Fril|label=}}
+===高階論理プログラミング===
+述語記号の項に、述語記号も含めるようにしている。例えば、<code>p(A, B, C) :- q(A, foo), r(B, bar), C.</code>では、Cを別個の述語記号にできる。テンプレートメタ的な書式も扱っており、例えば<code>p(A, B, C) :- (C)(A, B)</code>では、Cが述語名でAとBがその項になる。
+* {{仮リンク|λProlog|en|ΛProlog}}、{{仮リンク|HiLog|en|HiLog|label=}}
+=== 関数論理プログラミング ===
+述語記号と関数記号の双方をリテラルにしている。
+* {{仮リンク|Mercury言語|en|Mercury|label=Mercury}}、{{仮リンク|Curry (programming language)|en|Curry (programming language)|label=Curry}}
+=== オブジェクト指向論理プログラミング ===
+ファクトとルールをまとめた[[モジュール]]を扱っている。<code>module.predicate(A, B, C)</code>のように表記できる。モジュールは、[[オブジェクト指向]]由来の[[継承 (プログラミング)|継承]]と[[多態性]]を備えている。既存の上位モジュールを[[継承 (プログラミング)|継承]]して新規の下位モジュールを定義できる。上位モジュールの変数に下位モジュールを代入して[[サブタイピング]]するのが[[多態性]]である。例えば<code>var.predicate(A, B, C)</code>では、上位変数<code>var</code>に下位モジュールAを代入するとAの<code>predicate</code>と解釈され、同変数に下位モジュールBを代入するとBの<code>predicate</code>と解釈される。
+* {{仮リンク|Visual Prolog|en|Visual Prolog}}
+=== 線形論理プログラミング ===
+[[線形論理]]を扱っている。
+=== 帰納論理プログラミング ===
+[[帰納推論]]を扱っている。これまでの[[演繹論理|演繹推論]]とは別種になる。
+=== 仮説論理プログラミング ===
+[[仮説的推論|仮説推論]]を扱っている。これまでの[[演繹論理|演繹推論]]とは別種になる。
 ==適用分野==
@@ 59行目: / 145行目: @@
 ;[[自動定理証明]]
 : 既存の理論から新たな定理を生成するプログラム
-==歴史==
-論理プログラミングは人工知能の研究から生まれた考えであり、[[ジョン・マッカーシー]] [1958] の次の引用が確認されている最初の言明である。
-{{quote|適切な形式言語（おそらく述語計算の一部）を処理するプログラムは共通の手段となる。基本プログラムは前提から直ちに結論を導き出す。その結論は宣言的かもしれないし命令的かもしれない。命令的な結論が導かれるなら、そのプログラムはその結論に対応した動作をする}}
-[[ジョン・マッカーシー]]は彼の提案を以下のように補足した。
-{{quote|我々が ''advice taker'' に期待する主な利点は、その記号環境と探しているものについてセンテンスを入力するだけでシステムの動作が改良される点である。そのようなセンテンスを入力するにあたって、プログラムや advice taker に関する事前知識はほとんど必要としないだろう。advice taker は事前に教え込まれた知識から論理的に導き出される広範囲な能力を有していると仮定することができる。したがって、次のように言うことができるだろう。『事前知識を豊富に与えられ、自動演繹を行うプログラムは、常識を備えている』|}}
 ==関連項目==
-*[[形式手法]]
+*[[数理論理学]]
-*[[コンピュータ言語]]
+*[[述語論理]]
+*[[非単調論理]]
-**[[プログラミング言語]]
-***[[宣言型言語]]
+*[[導出原理]]
-****[[関数型言語]]
+*[[ホーン節]]
-****[[論理型言語]]
+*[[Prolog]]
+*[[Planner]]
-*****[[制約論理プログラミング言語]]
+*[[第五世代コンピュータ|第五世代コンピュータ計画]]
-*****[[解集合プログラミング]]
-*****[[並行論理プログラミング言語]]
-*****[[並行制約プログラミング言語]]
 == 脚注 ==
@@ 125行目: / 200行目: @@
 {{プログラミング言語の関連項目}}
+{{Normdaten}}
 {{DEFAULTSORT:ろんりふろくらみんく}}
 [[Category:論理プログラミング|*]]
 [[Category:プログラミングパラダイム]]

表話編歴コンピュータ・プログラミング言語の関連項目
言語水準	機械語 (1G) 低水準言語 (2G) 高水準言語 (3G) 第四世代言語第五世代言語
言語処理系	アセンブラインタプリタコンパイラトランスレータ
言語分類	マルチパラダイム言語命令型言語宣言型言語非構造化言語構造化言語非手続き型言語手続き型言語オブジェクト指向言語関数型言語論理型言語データフロー言語ダイナミック言語スクリプト言語軽量プログラミング言語ビジュアルプログラミング言語難解プログラミング言語
その他	ドメイン固有言語ジョブ制御言語問い合わせ言語マークアップ言語形式言語
関連項目	コンピュータ言語プログラミング言語一覧プログラミング言語年表プログラミングパラダイム