論理プログラミング

論理プログラミング（Logic Programming）は、述語論理を基礎にしたプログラミング技法である。人工知能の研究を主な目的にして始められた分野である。パターンマッチングを基軸にしたプログラムコード実行順序の選択決定が特徴である。アルゴリズムを論理式で宣言的に記述し、節形式で並べられた原子論理式を解釈する導出原理により手続き的に計算して求められた解答を推論するという、非決定性と失敗による否定を枠組みにしたパラダイムである。論理プログラミングは数々の応用サブパラダイムに分化されて実践されている。

1972年に初公開された「Prolog」が論理プログラミング言語の代表と見なされている。Prologは一階述語論理に準拠したホーン節による宣言的記述と、SLD導出による手続き的計算を特徴にしている。Prologを中心にした論理プログラミングの基礎は、1979年にロバート・コワルスキが発表した『Logic for Problem Solving』が現在に到るまでの規範にされている。

特徴

論理プログラミングは、手続き型/関数型/オブジェクト指向とは一線を画している独特な書式を持つ。本稿では論理型言語の代表とされるPrologベースのものを扱う。なお、Prolog系はどちらかと言うと簡素化重視の手続き的導出に偏った言語なので、論理プログラミングの標準的全貌とまでは言えないのが実情である。ユニフィケーションと呼ばれるパターンマッチングと代入概念が一切無い変数束縛と再帰限定は宣言的な純粋関数型パラダイムを彷彿とさせるが、ファクトと述語の登録/撤回という副作用の影響を全面的に受ける事になるユニフィケーションを通した変数束縛は全くの参照不透明になるのでこの点が手続き的となる。概形を掴むためにまず書式の見本例を以下に示す。

canfly(X) :- bird(X), not(abnormal(X)).
abnormal(X) :- wounded(X).
bird(john).
bird(mary).
wounded(john).

?- canfly(X).  %これがプログラム起点で（目標節）飛べるものを挙げよという質問になる

?-はコマンドプロンプトであり、そのcanfly(X)で実行開始される。(1)目標節のcanfly(X)は一行目のcanfly(X)とマッチする。(2)その対偶先のbird(X)は三行目のbird(john)とマッチしてbird(X=john)になる。(3)一行目のabnormal(X=john)は二行目のabnormal(X)とマッチする。(4)その対偶先のwounded(X=john)は五行目のwounded(john)とマッチするので一行目のnotで偽になり反駁される。(5)ここでbirdまでバックトラッキングされてXが白紙化される。(6)一行目のbird(X)は四行目のbird(mary)とマッチしてbird(X=mary)になる。(7)abnormal(X=mary)は反駁されるが、notで真になるので非反駁=成立になる。(8)一行目のcanfly(X=mary)が成立して目標節もcanfly(X=mary)となり、飛べるものはmaryという解が得られる。

節形式

本稿では節形式（clausal form）の代表格であるホーン節（horn clause）を扱う。ホーン節は単位節、確定節、目標節の三種に大別される。その構文は以下のようになる。目標節はプログラムにただ一つだけ存在しメインルーチンと同義になる。headとbodyはどちらもリテラル（原子論理式）を指す。リテラルは論理プログラミングにおける基本文である。1個以上のリテラルを連ねてピリオドで閉じたものが節（clause）となる。headはユニフィケーション先となるリテラルであり、bodyはユニフィケーション元となるリテラルである。

head.　　　　　　　　　　　%単位節。データまたは再帰停止条件になる
head :- body1, body2, ‥.　%確定節。body1かつbody2ならばheadという意味
?- body, ‥.　　　　　　　 %目標節。このbodyは質問になる

全てのリテラルは述語記号（predicate signature）になるので、プログラム的にはリテラル＝述語記号である。述語記号の書式は述語名(引数, 引数, ‥)である。述語記号が持つ引数の個数はアリティと呼ばれる。引数は定項引数（定数）と変項引数（変数）に分かれる。述語名は関手名（functor）と記号名（operator）に分かれる。関手名は任意のアトム（文字列）になるものであり、アリティは任意個数であり、ユニフィケーションされて命題定項になるものである。記号名は、等号式（=,≠）比較式（<, >, <=, >=）集合式（⊂, ⊃, ⊆, ⊇）束縛式（:=）などであり、いずれも2アリティであり、ユニフィケーションされないで命題定項になるものである。束縛式は論理的同値と同義であり変項（変数）束縛に用いられるが、実際にはユニフィケーションで束縛を行っている関手名の糖衣構文でもある。ユニフィケーション元の述語記号は、導出前は命題変項と同義の存在になり、導出後は命題定項（真または偽）になる。

単位節（unit clause）は、1個のheadリテラルから成る。変項引数を含まないリテラルはファクトと呼ばれる。ファクトはグローバルデータと考えてよいものであり、構造体（述語名＝タグ、引数＝フィールド）とも見れるものになる。空リストや0や1といった数値の引数を持つリテラルは、ユニフィケーション再帰停止条件として使われる。確定節（definite clause）は、1個のheadリテラルと1個以上のbodyリテラルから成る。headとbody群は論理包含記号:-で繋がれる。headは論理包含の後件（consequent）であり、body群は前件（antecedent）である。headリテラルはユニフィケーション照合先になり、bodyの各リテラルはユニフィケーション照合元になる。headリテラルの対偶である各bodyリテラルの導出が全て真になると、そのheadリテラルへのユニフィケーション元のリテラルも真になって成立し、そのリテラルの変項引数への双方向性（⇔）束縛も成立する。目標節（goal clause）は、1個以上のbodyリテラルから成る。左からのbodyリテラルがユニフィケーション元になってプログラムは実行開始される。目標節の左端記号?-はfalse :-の省略形であり、このfalseとは導出原理の最後に現れる空節（empty clause）を意味しているが、プログラム的には特に意識する必要はない。

項

項（term）は論理プログラミングにおける情報要素である。単純項は、述語記号の引数、リストの要素、関数記号の引数といった形態で存在する。単純項はいわゆる動的型付けであり型注釈といった概念は無く、数値（整数、有理数、実数）かアトム（文字列）かの区別はシステム側が自動判別する。

単純項（simple term）

• 定項（constant term）
  • アトム（atom）- 文字列のこと。この世に存在するあらゆる個体（individual）を特定するための任意名識別子である。
  • 数値（number）- 計算可能な数値。実装レベルでは整数、有理数、実数（浮動小数点）などに分化されている。
• 変項（variable term）
  • 自由変項（free variable ）- 定項が束縛されていないもの。無名変項も指す。
  • 束縛変項（bound variable ）- 定項が束縛されているもの。その定項と論理的同値になる。
• 関数記号（function signature）- 数値のための計算記号であり+, -, *, /, ^, √, !, などである。数値と変項を引数にし1～2アリティである。関数記号は評価前のネーム（name）または評価後の数値のどちらかの形態を取れる。

複合項（compound term）

• ファクト（fact ）- 事実。引数が全て定項の関手述語。0アリティの関手述語、偽の命題定項（fail）も指す。
• 述語記号（predicate signature）
  • 関手述語（functor predicate）- アトムを述語名とするもの。
  • 記号述語（operator predicate ）- 等号式、比較式、集合式、束縛式といった記号を述語名とするもの。
  • 組込命令述語（command predicate ）- 各種入出力やシステムコールなどのいわゆるAPI命令。カットオペレータも指す。
• リスト（list ）- 項集合の表現体である。リストとは正確には項と入れ子リストのペア表現を指しており[term|list] と書式される。termは定項、変項、リストのどれかを指し| でlist と連結される。入れ子リストを指すlistは再帰する。空リストは[] と書式されリスト末端表現にもなる。要素を列挙できる[2, 4, 8] [A, B, C|list] などの書式は糖衣構文 であり、実際には上述のペア表現の再帰で実装されている。

導出原理

論理プログラミングにおける導出（resolution）とは、照合元と照合先の論理式を持ち寄り、双方の定項と変項を相互に束縛し合って互いの変項部分を特定し、変項が特定された状態の照合先論理式の真偽判定を行なう作業を指す。その真偽判定の中では再帰的な真偽判定が繰り返されることになり、それら一連の反復作業の遂行方針を導出原理（resolution principle）と呼ぶ。導出原理から得られた真は目標節での質問にされた事実の成立解答になり、その事実内変項の束縛内容は質問された未知要素解答になる。真が得られなかった場合は事実の不成立解答になり、未知要素も分からずじまいとなる。本稿で扱っているホーン節は、論理包含の後件に当たるheadリテラルを一つに限定している表現であり、そのホーン節用の導出原理であるSLD導出（selective linear definite clause resolution）はユニフィケーションの方向性をbodyリテラルからheadリテラルに限定している計算である。目標節の左端bodyリテラルから始まるユニフィケーションは、サブルーチン呼び出しに当たるものと考えてよい。ユニフィケーションとは、照合元bodyリテラルとマッチングするheadリテラルをサーチして互いの引数同士を束縛し合って、その照合先headリテラルの対偶:-のbodyリテラル群の導出に移る仕組みを指す。マッチングは述語名が一致し、アリティが同じであり、各引数の照合が下記の通りならば成立する。

• 照合元引数が定項ならば、照合先引数が同一定項か、同一内容の束縛変項か、自由変項ならば引数マッチングする。
• 照合元引数が束縛変項ならばその内容と、照合先引数が同一定項か、同一内容の束縛変項か、自由変項ならば引数マッチングする。
• 照合元引数が自由変項ならば、無条件で引数マッチングする。

論理プログラミングではCPUパフォーマンスの多くをこのマッチングサーチが占める。ユニフィケーションの結果、照合先headリテラルの対偶:-の全bodyリテラル引数の自由変項はユニフィケーション時内容を当てはめた束縛変項に変えられる。自由→束縛変項になった状態のリテラル群は導出節と呼ばれる。導出節の左端のbodyリテラルが次のユニフィケーション照合元になってマッチングサーチするを繰り返す。マッチングサーチは原則的にプログラム内にある単位節と確定節を全て走査する決まりなので、どこかでマッチングした時はその次の走査位置がスタックに積まれる。マッチング節の導出が失敗した時はスタックされた走査位置に戻る。これをバックトラッキングと言う。なお、照合元がファクト（全引数が定項）だとユニフィケーションではなくパターンマッチングになる。照合元bodyリテラルの自由変項に、照合先headリテラルから束縛された内容は、サブルーチン呼び出しのリターン値に当たるものになる。これはバックトラッキングが発生すると取り消されることになる。照合元bodyリテラルの自由変項の内容は解放されて空欄になり、スタックから取り出された次の走査位置からのマッチングサーチに再び移行される。

非決定性と失敗による否定

ユニフィケーションによるマッチングサーチは原則的にプログラム内にある全ての単位節と確定節を走査する決まりなので、途中のマッチング節が真になって走査から抜けても、次の節位置のスタックは残されることになる。そのまま導出原理が最終的な真まで到っても、スタックが残っている限り、そのスタックからの別の導出過程（遷移表）の可能性も残されていることになる。ここでスタックに積まれた走査位置に戻ることもバックトラッキングと言う。バックトラッキングによって目標節bodyリテラルの引数変項に当てはめられる内容は複数導出されることがある。オペレータは一つの解答を得ても選言記号を入力して他の解答を得られる。この性質は複数の遷移表を持つ非決定性チューリングマシンに因んで非決定性（nondeterministic）と定義されている。

マッチングサーチは最後まで走査し切ると真節発見不可という意味での偽が返るので、論理プログラミングのデフォルト終了状態は常に偽に行き着く。目標節の?-（false :-）はこれも意味している。ただしこの偽（false）は事実の否定（negation）ではない。偽に行き着く前に一度でも真を導出できれば失敗（failure）ではなくなり事実は否定されない。一度も真を導出できなかったら失敗になり事実は否定される。この閉世界仮説に則った性質は、失敗による否定（negation as failure）と定義されている。スタックは節内のカットオペレータによって任意に削除できるので無駄なバックトラッキングを回避できる。また、目標節のbodyリテラルが真偽二択のファクトならば一度の真で事足りるので、真の導出後にスタック全カットになるのが普通である。カットオペレータが用いられた場合のプログラムは真（true）の状態で終了する。

フロー制御構造

ホーン節での条件分岐は、カットオペレータとバックトラッキングを利用する形で表現される。下の例では一行目then節のカットオペレータでバックトラッキングが発生しないので二行目else節は走査されない。もし入力年齢が20の場合は一行目のAge<13で偽になるのでバックトラッキングされて二行目のelse節に移る。

 ticket(Age, Money) :- Age < 13, !, Money is 500. % then節。!はカットオペレータ
 ticket(_, Money) :- Money is 1000. 　　　　　　　% else節。_は無名変項

 ?- ticket(10, Money). 　　　　　　　　　　　　　 % 10歳のチケット金額は？
 Money = 500

ホーン節でのループ処理は、ユニフィケーションの再帰で行われる。カウンタ上限/下限値や空リストを引数にした単位節が再帰停止条件にされることが多い。下の例では一行目の引数「1」がカウンタ下限値である。二行目の節内で逐次登録される束縛変数Cが言わばループカウンタである。

 retrieve(1, [X|_], X).
 retrieve(N, [_|Ls], X) :- N > 1, C is N-1, retrieve(C, Ls, X).

 ?- retrieve(5, [1,2,4,8,16,32,64,128,256,512,1024], X). %リストの五番目は？
 X = 16

歴史

自動定理証明とAdvice taker

論理プログラミングは自動推論分野に端を発しているものであり、そのルーツは1950年代から盛んになっていたコンピュータによる自動定理証明と、1958年にマサチューセッツ工科大学（MIT）のジョン・マッカーシーが開発したプログラミング言語「LISP」にまで遡ることが出来る。LISP誕生の背景には自動推論の発展形としての人工知能（AI）に対する研究があり、自動定理証明における演繹法（=導出原理）をより汎用的な推論アルゴリズムに拡張しようとする試みがあった。マッカーシーはLISP公開当初の設計を、記号式の再帰関数群とそれらの計算（recursive functions of symbolic expressions and their computation by machine）という題目で説明している。同1958年にマッカーシーは、人工知能のキーポイントとなる常識推論（commonsense reasoning）の実現に向けたプログラミングパラダイム仮説も発表している。Advice takerと題された以下の仮説は、論理プログラミングの原型構想と言えるものであった。

述語論理に似た適切な形式言語を扱うプログラムは共通有用ステートメントになる。プログラムとは数々の前提から率直に結論を導き出せるものである。その結論は命令的判決または宣言的判決のどちらかになる。命令的判決ではそれに応じた機器操作も行われる。我々がadvice takerに期待するもの―それは最小限のステートメントで最大限の有用性が得られることである。ステートメントは最小限の知識定義しか要求しない。advice takerは保有知識と与えられたヒントから論理的に解答できる。解答は公式知識に基づく常識推論に沿ったものである。従って我々はこう言える。プログラムはcommon senseを備えていると。

節形式と導出原理の確立

マッカーシーは現在の論理プログラミングの姿に繋がるアイディアを直接出すことはなく、彼の自動推論＝人工知能研究はあくまでLISPの発展を通したものになった。1965年頃に当時スタンフォード大学に在籍していたコーデル・グリーンが、節形式（clausal form）の論理式アルゴリズム書式を初めて発表した。グリーンは節形式を解釈するための導出原理（resolution principle）も考案し、双方を合わせた宣言的言語はLISPの試験的方言として実装されている。グリーンの導出原理は、ジョン・アラン・ロビンソンが発表していた一階述語論理準拠の単一化を自動定理証明に組み込んだ命題論理背景の演繹法＝導出原理を参考にしていた。ここで論理的（logical）と手続き的（procedual）という典範上（epitomize）の対立が生まれた。自動定理証明の視点に立つロビンソンとグリーンによると、LISPのフォーム（リスト化された式）と関数再帰の多用は論理的ではない邪道（cheating）な手続き的であるとされ、ここから自動定理証明と人工知能研究の分岐も始まっている。人工知能研究を目的にした数々のLISP方言が考案されていく中で、1967年のアバディーン大学で現在の論理プログラミングの姿に近い初めての言語に位置付けられている「Absys」が発表されている。

宣言的表現 vs 手続き的表現

1960年代を通して人工知能および論理プログラミング研究者たちの間では、宣言的表現と手続き的表現のどちらを採用するべきかという問題を巡って活発な議論が行われていた。この表現上（representation）の対立では、主に知識の埋込（embedded of knowledge）方法と二階述語論理の導入方式が対象になっていた。宣言的表現（declarative）を提唱したのは、スタンフォード大学とエディンバラ大学を中心にした研究者たちであり、ジョン・アラン・ロビンソン、コーデル・グリーン、バートラム・ラファエルパット・ヘイズロバート・コワルスキたちが名を連ねていた。それに対する手続き的表現（procedural）を提唱したのは、マービン・ミンスキーとシーモア・パパートが主導するマサチューセッツ工科大学在籍の研究者たちであった。宣言的表現を重視する研究者たちは自動定理証明に沿った論理学または数理論理学のアルゴリズムに忠実であることを望んでいた。手続き的表現を重視する研究者たちはプログラム実装に合わせて最適化されたアルゴリズムの導入に前向きだった。

Plannerの開発

1969年、マサチューセッツ工科大学（MIT）のマービン・ミンスキーとシーモア・パパートが主導する研究チームの中でカール・ヒューイットが言語仕様をデザインした論理型言語「Planner」が初回稼働された。Plannerはメインフレーム運用を前提にした大規模な言語であり、画一的な定理証明手法の否定と手続き的な知識の埋め込み手法を理念にして、情報群および知識定義からの節形式への柔軟な変換表現と、前向き連鎖と後向き連鎖の双方を備えた柔軟な導出原理が実装されていた。Plannerの大規模さは運用できる環境を限定したので、1971年にポータビリティを重視したPlannerのサブセット版である「Micro-Planner」が、ジェラルド・サスマン、ユージン・チャニアクテリー・ウィノグラードらによって開発された。Micro-Plannerは主に自然言語解析に用いられて当時の著名な自然言語処理プログラムであるSHRDLUを誕生させている。同時期にSRIインターナショナルのリチャード・ウォルディンガーらは、Planner処理系上で稼働するデータマイニングの先駆的プログラムであるQA4を開発し、これは更に言語仕様を組み込んだ「QLISP」に拡張されてInterlisp上で実装された。

1971年にパパート、サスマン、チャニアク、ウォルディンガーといったMITの面々がエディンバラ大学を訪問し、彼らの成果物であるMicro-PlannerとSHRDLUを披露した。当時のエディンバラ大学は自動定理証明プロジェクトLogic for computable functionsが始動されていた人工知能ロジック分野のメッカであった。パパートたちが披露した手続き的表現の導出原理を目の当たりにしたパット・ヘイズは、自動定理証明を奉じる宣言的表現の導出原理は過去の遺物と化しているのではないかと考えるようになった。Micro-Plannerのサブセット版である「Pico-Planner」がエディンバラ大学でも直ちに実装されてその有用性が確認された。ヘイズは、自動定理証明の研究に従事していたロバート・コワルスキにPlannerを参考にするように勧めた。Plannerの研究を注意深く始めたコワルスキは、自身が構想していた節形式とそれに対するselective linear導出に近いものをPlannerの中に認め、ここからの着想がホーア節とSLD導出の発表に繋がることになった。更にエディンバラ大学ではその価値を認めたPlannerでカバーできなかった仕様をも補完実装した論理型言語「Popler」が開発されている。

Prologの開発

1971年、ロンドン開催の国際人工知能会議に出席してPlannerに強い関心を抱いていたアラン・カルメラウアーらは、ロバート・コワルスキとテリー・ウィノグラードの両名からレクチャーを受けて、マルセイユ大学で従事していた自動推論各分野研究のための言語処理系の構築に着手した。彼らの決意は翌1972年に結実し、コワルスキが発表していたホーン節とSLD導出を取り入れた論理プログラミング言語「Prolog」が誕生した。Prologに対する意見は分かれ、MITのカール・ヒューイットなどはMicro-Plannerの複製品であると言及し、エディンバラ大学のコワルスキは論理プログラミングへの良いアプローチであると評した。マルセイユ大学のカルメラウアーの下で実装されたインタプリタ式の元祖版Prologは「Marseille Prolog」と呼ばれるようになった。後にカルメラウアーは元祖の後継版も発表しているが、彼のマルセイユ系統はPrologのメインストリームにはならなかった。Prologに注目したコワルスキの門弟であるデビッド・ウォーレンがエディンバラ大学で再構築したものは「Edinburgh Prolog」と呼ばれ、よりモダン化された書式でPrologを普及させる原動力になった。ウォーレンは1977年にコンパイラ式のPrologも開発し、こちらは実装運用マシンに因んで「DEC-10 Prolog」と呼ばれ、Prolog言語仕様のスタンダードに位置付けられた。1979年、エディンバラ大学からインペリアル・カレッジ・ロンドンに移っていたコワルスキは、論理プログラミング基礎の集大成となる『Logic for Problem Solving』を上梓した。1983年、SRIインターナショナルに移籍していたウォーレンは、Prologコンパイラ実装のための標準処理系規範となるウォーレン抽象マシンを策定してPrologの更なる普及に努めた。1986年に論理プログラミング協会が設立され、IOS標準化に向けた準備も始められた。1987年にDEC-10 Prologの流れを汲む「SWI-Prolog」がアムステルダム大学のジャン・ウィールメーカーによって開発され、これが現在最も広く使われているProlog言語として知られている。

1980年代の日本の情報工学分野ではPrologに対する積極的な研究が行われていた。1970代半ばにSRIインターナショナルに留学していた日本人研究員が目にしたマルセイユPrologを、当時の電子技術総合研究所に持ち帰ったのがその発端である。同研究所で自動推論部門と自然言語処理部門を担当する重職に就いていた渕一博が、Prologを重要視するようになり、彼の提案が採用されて1982年に新世代コンピュータ技術開発機構（ICOT）が設立され、第五世代コンピュータと名付けられた一大プロジェクトが発足した。その目的は非ノイマン式で運用される知識情報処理と定義された人工知能コンピュータの開発であり、その人工知能プログラミング技術の中心にはPrologベースの並行論理プログラミングが据えられた。

論理プログラミングの派生

並行論理

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

並行論理（Concurrent logic）は、ユニフィケーション時のリテラルマッチングからの導出をマルチスレッドで並行実行できるようにした応用パラダイムである。スレッド資源がある限りバックトラッキングが発生しなくなるので大幅に高速化される。並行論理でのホーン節は、head :- guard | body.のようになる。guardリテラルでスレッド同期が取られる。guardリテラルで扱われる「同期用変項」は、スレッド間でシェアされる再代入可能変数になっている事が多く、ロック変数、セマフォ変数、バリア変数などに近いものになっている。この分野の主な研究者にはキース・L・クラーク、エフド・シャピロ、上田和紀などがいる。前述の第五世代コンピュータ計画は並行推論システムの構築を基幹にしていた。

• Concurrent Prolog
• PARLOG
• GHC
• KL1

制約論理

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

制約論理（Constraint logic）は、単純項に「制約」（constraint）という要素を加えた応用パラダイムである。制約とは領域（domain）と個体（individual）の間に横たわるあらゆる中間状態を指している。領域とは数学の集合に相当するものであり、個体とは値（定項）である。領域は全称量と同義になり、制約は存在量と同義になる。制約は述語記号の引数とリストの要素になって情報要素の柔軟な表現を可能にする。

• B-Prolog
• Ciao
• ECLiPSe
• Fril

並行制約論理

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

並行制約論理（Concurrent constraint logic）は、並行論理欄で説明した「同期用変項」を、制約論理欄で説明した「制約」にした応用パラダイムである。制約化された同期用変項はプロセス代数と同じものになる。この同期用制約とアクターモデルの親和性を見出した計算機科学者ビジェイ・サラスワットとケネス・カーンは、アクターモデルは並行制約プログラミングの特別なケースであると主張した。アクターモデルはPlanner開発者のカール・ヒューイットが提唱した並行計算理論である。

• Oz
• ToonTalk
• アリス

仮説論理

仮説論理（Abductive logic）は、リテラル（述語記号）から導出される命題定項を、制約論理欄で説明した「制約」にした応用パラダイムである。この制約はファジー論理と読み替えてもよい。通常の論理プログラミング（バニラ論理）のリテラル導出からは真か偽の命題定項が返るだけだが、仮説論理ではそれに加えて制約＝ファジー論理＝仮説述語記号（abducible predicate）も返されるようにしている。真偽の決定に到らなかったことを表わす仮説述語記号とは、その真偽の決定に必要と見なされた述語記号を連ねた論理式といったものになる。仮説述語記号は偽ではないので次のリテラル導出に進むことになる。右端のリテラル導出が終わったらそれまでに列挙されていた仮説述語記号をまとめた論理式（真と偽の中間状態である制約）がユニフィケーション元に返されることになる。バニラ論理では真が得られない＝偽になった時点で導出不可になるが、仮説論理ではそのまま導出を継続してその過程で得られた定項を、保留しておいた仮説述語記号に当てはめて再度の導出を試みるといった柔軟な導出原理が可能になる。仮説述語記号はコンピュータによる問い返しでもあるので、これを記録（記憶）しておくことは機械学習への動機および筋道にもなる。仮説論理はその性質から言語処理系を中心にしたフレームワークとして実装されるのが一般的である。

• ACLP System
• Asystem

帰納論理

帰納論理（Inductive logic）は、制約論理と仮説論理のハイブリッド的な応用パラダイムである。仮説論理欄で説明した仮説述語記号の仕組みに加えて、返された仮説述語記号に対して制約論理欄で説明した「制約」を当てはめるようにして再度の導出成功を早めるようにしたものである。制約には100<X<200のような計算領域や、列挙型に相当する有限領域（finite domain）など幾つかの種類がある。制約内にある個体（定項）を一つ一つ総当たりで仮説述語記号の引数箇所に当てはめて導出を試みるという手法が帰納になる。帰納論理もその性質から言語処理系を中心にしたフレームワークとして実装されるのが一般的である。

• Aleph
• Atom
• DL-Learner
• FOIL
• ILASP
• Inthelex

従来の拡張およびマイナーな派生

高階論理

高階論理（Higher-order logic）は、変項に述語記号も束縛できるようにした応用パラダイムである。その変項はリテラルとして配置できる。p(A, B, C) :- q(A, foo), r(B, bar), C.のようになり、Cが述語記号束縛変項である。述語記号を連ねた節も変項に束縛できる。アトムから述語記号/節を連想束縛できる組み込みマッピングも用意されている。(P)(A, B)という書式では、Pに束縛されたアトムを述語名にしてAとBを引数にした述語記号になる。高階述語論理準拠に従って引数AとBもまた述語記号/節にできる。高階論理はメタプログラミング的な柔軟な論理式表現を可能にする。

• λProlog
• HiLog

関数論理

関数論理（Functional logic）は、述語記号と関数記号の双方をリテラルにした応用パラダイムである。関数記号は確定節の形式で自由に定義できて、headが関数プロトタイプになり、body群が関数式内容になる。述語記号のユニフィケーション/パターンマッチングからは命題定項（真か偽）のみが返されて偽ならその節からバックトラッキングされる。変数仕様は再代入のない束縛のみに限られているものである。論理型と純粋関数型の中間的パラダイムであるが、関数から新たな関数を導出するという二階述語論理準拠の仕様が無いのが大きな違いになる。

• Mercury

オブジェクト指向論理

オブジェクト指向論理（Object-oriented logic）は、一定の単位節と確定節をまとめたクラスまたはモジュールの仕様を採用している応用パラダイムである。ここではモジュールとする。module.predicate(A, B, C)などのようにリテラルを表記できる。モジュールは継承と多態性の機能を備えている。継承は既存モジュールに任意の単位/確定節のまとまりを付け足した新規モジュールを定義できる差分プログラミング用の機能である。多態性はその付け足し部分を動的に切り替えられる機能であり、同じ述語記号から実行時状態に応じた別々のユニフィケーションと導出が得られるようになる。

• Visual Prolog

関連項目

• 自動推論
• 自動定理証明 - 既存の理論から新たな定理を生成するプログラム
• 自然言語処理
• エキスパートシステム - 特定応用分野の巨大なモデルから、推奨や回答を生成するプログラム
• 人工知能
• 宣言型プログラミング

参考文献

• 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.

外部リンク

• Logic Programming Virtual Library entry
• Bibliographies on Logic Programming
• Association for Logic Programming (ALP)
• Theory and Practice of Logic Programming journal
• Logic programming in Oz