ユニフィケーションのソースを表示

{{otheruses||その他|統一}}
'''ユニフィケーション'''（{{lang-en-short|unification}}）は[[数理論理学]]や[[計算機科学]]の用語であり、{{仮リンク|充足性|en|satisfiability}}問題を解く際のアルゴリズム的プロセスである。ユニフィケーションは、見た目の異なる2つの{{仮リンク|項 (論理学)|en|term (logic)|label=項}}が[[恒等式|同一]]<ref>{{lang-en-short|identical}}</ref>または[[等式|同等]]<ref>{{lang-en-short|equal}}</ref>であることを示す{{仮リンク|置換 (論理学)|en|Substitution (logic)|label=置換}}を求めるのが目的である。ユニフィケーションは[[自動推論]]、[[論理プログラミング]]、プログラミング言語の[[型システム]]の実装などに幅広く用いられている。

なお、ユニフィケーションを'''単一化'''あるいは'''統一化'''とも呼ぶ。

主なユニフィケーションは数種類ある。等号を持たない論理（理論）において、2つの項が[[恒等式|同一]]であることを示すためのユニフィケーションは'''統語論的ユニフィケーション'''<ref>{{lang-en-short|syntactic unification}}</ref>と呼ばれる。空でない等号を持つ論理（理論）で2つの項の[[等式|同等性]]<ref>{{lang-en-short|equality}}</ref>を示す場合、それを'''意味論的ユニフィケーション'''<ref>{{lang-en-short|semantic unification}}</ref>と呼ぶ。置換は[[順序集合]]として順序付けられるので、ユニフィケーションは[[束 (束論)|束]]における[[結び (数学)|結び]]を求める手続きとして解釈できる。

ユニフィケーションアルゴリズムは[[ジャック・エルブラン]]<ref>J. Herbrand: Recherches sur la théorie de la démonstration. ''Travaux de la société des Sciences et des Lettres de Varsovie'', Class III, Sciences Mathématiques et Physiques, 33, 1930.</ref><ref>{{cite report | author1=Claus-Peter Wirth |  author2=Jörg Siekmann | author3= Christoph Benzmüller | author4= Serge Autexier | title=Lectures on Jacques Herbrand as a Logician | institution=DFKI | type=SEKI Report | number=SR-2009-01 | year=2009 | arxiv=0902.4682 }} Here: p.56</ref><ref>{{cite thesis | type=Ph.D. thesis | url=http://www.numdam.org/issue/THESE_1930__110__1_0.pdf | author=Jacques Herbrand | title=Recherches sur la théorie de la demonstration | institution=Université de Paris | series=A | volume=1252 | year=1930 }} Here: p.96-97</ref>によって最初に発見されたが、ユニフィケーションを初めて形式的に研究したのは{{仮リンク|ジョン・アラン・ロビンソン|en|John Alan Robinson}}で、一階述語論理の[[導出]]手続きを構築する際に一階のユニフィケーションを基盤として使い、[[組合せ爆発]]の原因の1つ（項を例化したものの探索）を排除することで自動推論技術への大きな一歩とした。

== 一階の項の統語論的ユニフィケーション ==
=== 一階の項 ===
変数記号の集合 X = {x,y,z,...}、個別定数記号の集合 C = {a,b,c,...}、個別関数記号の集合 F = {f,g,h,...} が与えられたとき、「項」は以下のような有限個の規則を適用して得られる式として定義される。

*'''基本''': 任意の変数 <math>x \in X</math> および任意の定数 <math>a \in C</math> は、それぞれ項である。
*'''帰納''': <math>t_1,\ldots,t_k</math> が項なら <math>f(t_1,\ldots,t_k)</math> も項である。ただし k は正の有限の整数。

例えば、x、y、a、b は基本規則から項であることが明らかである。f(a,x) や g(b,y,x) は基本規則で項とされたものに帰納規則を一回適用することで得られる。f(a,f(a,x)) は帰納規則を2回適用することで得られる。このように様々な項が生成できる。簡単にするため、定数記号は引数（アリティ）がゼロ個の関数記号とみなすことが多く、帰納規則でゼロ引数の項も許容されるようにする。その場合、a() は a と統語論的に同等である。証明を行う目的では、基本規則と帰納規則を明確に区別するため、定数（ゼロアリティ関数）とアリティがゼロより大きい関数記号とを区別する。数学では関数記号ごとに引数の個数（アリティ）を固定することが多いが、統語論的ユニフィケーション問題では一般に関数記号は（有限の）任意個の引数を持ち、同じ関数記号であっても文脈によって異なる個数の引数をとりうる。例えば、f(f(a),f(x,y,z)) はユニフィケーション問題においては正しい項である。

=== 置換 ===
置換は、変数から項へのマッピングの有限集合 <math>\{ x_1 \mapsto t_1,\dots, x_k \mapsto t_k \}</math> と定義され、1つの変数を2つの異なる項にマッピングすると曖昧さが生じるため、個々のマッピングは一意的でなければならない。項 u への置換の「適用」を <math>u \{ x_1 \mapsto t_1,\dots, x_k \mapsto t_k \}</math> と記述し、項 <math>u</math> に出現する各変数 <math>x_{i}</math> を項 <math>t_{i}</math> で置き換えることを意味する。このとき、<math>1\leq i \leq k</math> である。例えば、<math>f(x,a,g(z),y) \{ x \mapsto h(a,y), z \mapsto b  \} = f(h(a,y),a,g(b),y)</math> となる。

=== 一階の項における統語論的ユニフィケーション問題 ===
一階の項における統語論的ユニフィケーション問題は、同等である可能性のある有限個の式の連言 <math>t_1 \stackrel{?}{=} u_1 \And, \ldots, \And t_n \stackrel{?}{=} u_n</math> で表される。この問題を解くには、それぞれの潜在的等式の左辺と右辺が統語論的に等価となるような置換 <math>\theta</math> を求める必要があり、<math>t_1\theta = u_1\theta \And, \ldots, \And t_n\theta = u_n\theta</math> となるようにしなければならない。そのような置換 <math>\theta</math> を「単一子」（ユニフィケーション作用素）と呼ぶ。ユニフィケーション問題には解がない場合もある。例えば、<math>x\stackrel{?}{=} z \And y \stackrel{?}{=} f(x)</math> の単一子は <math>\{ x \mapsto z, y \mapsto f(z) \}</math> である。この場合、

:<math>x \{ x \mapsto z, y \mapsto f(z) \} = z = z \{ x \mapsto z, y \mapsto f(z) \} = z</math> 
:<math>y\{ x \mapsto z, y \mapsto f(z) \} = f(z) = f(x)\{ x \mapsto z, y \mapsto f(z) \} = f(z)</math>

となる。

=== 出現検査 ===
変数 ''x'' を ''x'' が部分として出現する関数 ''x=f(...,x,...)'' とユニフィケーションしようとする場合、''x'' は無限個の項を持たなければならなくなる。これは有限であるとした項の定義と矛盾するため、ユニフィケーションは失敗する。そのためユニフィケーション問題を解くアルゴリズムでは、まず ''x'' がユニフィケーションしようとする項の中に出現しないかチェックする。これを{{仮リンク|出現検査|en|Occurs check}}<ref>{{lang-en-short|occurs check}}</ref>などと呼ぶ。

== 非形式的概要 ==
2つの項 <tt>s</tt> と <tt>t</tt> があるとき、（統語論的）ユニフィケーションは <tt>s</tt> と <tt>t</tt> を構造的に等価にする置換を求めるプロセスである。そのような置換が存在する場合、それを <tt>s</tt> と <tt>t</tt> の'''単一子'''<ref>{{lang-en-short|unifier}}</ref>と呼ぶ。

理論上、入力された2つの項は無数の単一子を持ちうる。しかし一般的用途では1つの'''最大汎用単一子'''<ref name="#1">{{lang-en-short|most general unifier}}</ref>を考慮すれば十分である。他の単一子は最大汎用単一子のインスタンスである。

一階のユニフィケーションは、[[一階述語論理#項|一階の項]]（変数記号や関数記号で構築される項）の統語論的ユニフィケーションである。一方高階ユニフィケーションは、高階の項（何らかの高階の変数を含む項）のユニフィケーションを指す。

特定のユニフィケーションアルゴリズムの理論的属性は、入力される項の多様性に依存する。たとえば一階のユニフィケーションは決定可能であり、単一化可能な項群は必ず最大汎用単一子を持つ。しかし高階ユニフィケーションは一般に決定不能であり、最大汎用単一子を持たないことが多い。

統語論的ユニフィケーションとは別に、'''意味論的ユニフィケーション'''<ref>{{lang-en-short|equational-unification}}。{{lang|en|e-unification}} とも呼ばれる。</ref>も広く使われている。この2つは、項を「等しい」とみなす方法が異なる。統語論的ユニフィケーションでは、置換によって項が構造的に等価になるようにする。意味論的ユニフィケーションでは、2つの項が何らかの理論において合同であるかで判定する。例えば、[[交換法則|交換性]]と[[結合法則|結合性]]において合同な項を「等しい」とするユニフィケーションをAC-ユニフィケーションと呼ぶ。

ユニフィケーションは計算機科学の重要なツールである。特に一階のユニフィケーションは[[論理プログラミング]]、プログラミング言語の[[型システム]]設計、[[自動推論]]などに用いられている。高階ユニフィケーションは定理証明支援で使われている。高階ユニフィケーションに制約を加えたものを実装に採用したプログラミング言語<ref>{{lang|en|lamdaProlog}}など</ref>もある。意味論的ユニフィケーションは、背景理論付きSAT (SMT) を解くアルゴリズムや[[項書き換え]]アルゴリズムでよく使われている。

== 一階述語論理でのユニフィケーションの定義 ==
p と q が[[一階述語論理]]の文とする。
:UNIFY(p,q) = U ここで subst(U,p) = subst(U,q)

subst(U,p) は置換 U を文 p に適用した結果を意味する。したがって U は p と q にとっての'''単一子'''である。p と q のユニフィケーションは両者に U を適用した結果である<ref>Russell, Norvig: Artificial Intelligence, A Modern Approach, p. 277</ref>。

例えば L = {p,q} のような文の集合 L があるとする。L についての全単一子を U' としたとき、L に U を適用したものにある置換 s を適用した結果が L に U' を適用した結果と同じなら、単一子 U は L の'''最大汎用単一子'''<ref name="#1"/>と呼ばれる。
:subst(U',L) = subst(s,subst(U,L)).

== 論理プログラミングでのユニフィケーション ==
'''単一化(ユニフィケーション)'''の考え方は {{lang|en|[[Prolog]]}} に代表される[[論理プログラミング]]の根底を支える重要な概念である。それは変数の内容の[[名前束縛|束縛]]であり、項の構成要素の全体の形式から細部までその同一性を検査する機構である。他のプログラム言語とは異なり、{{lang|en|Prolog}} では <tt>=</tt> という記号はこの意味を表す。{{lang|en|Prolog}} は、質問としての副目標と、これによって呼び出される述語定義の頭部の単一化が試みられ、頭部の単一化の成功した節のみ選択され、その本体が次の質問になる導出と呼ばれるダイナミックで再帰的な機構によって実行される。

一般に[[型推論]]アルゴリズムは上記単一化に基づいている。

{{lang|en|Prolog}} では、単一化されるとは、
# 束縛されていない[[変数 (数学)|変数]] は、原子項、複合項、そして他の束縛されていない変数を、以後同一なものとみなす。この変数の変数名を、変数を含む他の項の一種の別名と解釈することも可能である。全ての形式の項に対して同一のものとみなすことができるのだから、束縛されていない変数の単一化は必ず成功する。(注1)
# 原子項（アトム）は同じ原子項とだけ単一化可能である。原子項はアルファベット(英文字に限らない)によって構成された文字列なのでこの先頭から最後までの文字とその位置が同一の場合、単一化される。一ヶ所でも異なれば単一化は失敗する。
# 複合項は関数名(述語名)と[[アリティ]]（オペランドの個数）が等しい場合に、対応するオペランド毎に項の単一化が再帰的に試みられる。この単一化が全て成功した場合のみ単一化に成功したことになる。

(注1) 最近の {{lang|en|Prolog}} や[[一階述語論理]]では、変数（変項）はそれ自身を含む項と単一化することはできない。それをすると無限の単一化が発生するためである。

== 型推論 ==
ユニフィケーションは[[型推論]]でも使われており、例えば関数型言語 {{lang|en|[[Haskell]]}} で使われている。型推論を行う言語では型に関する情報をいちいち記述する必要がなく、ユニフィケーションはデータ型の誤り検出に使われる。Haskellの式 <nowiki>1:['a','b','c']</nowiki> は型付けが正しくない。なぜならリスト構築関数 <code>:</code> の型は <code><nowiki>a->[a]->[a]</nowiki></code> だが、第一引数 <code>1</code> からポリモルフィックな型変数 <code>a</code> はInt型となるのに対して、<code><nowiki>['a','b','c']</nowiki></code> の型は<code><nowiki>[Char]</nowiki></code>であり、<code>a</code> は同時に <code>Char</code> と <code>Int</code> になることはできないからである。

型推論のアルゴリズムは次のようになる:

# 任意の型変数は任意の型表現と単一化し、その表現をインスタンス化する。理論によっては出現検査でこの規則に制約を課すこともある。
# 2つの型定数は両者が同じ型のときのみ単一化される。
# 2つの型構築は、両者が使用する型構築子が同じで、それらのコンポーネント型が再帰的に単一化されるときのみ単一化される。

宣言的特徴から、ユニフィケーションが行われる順序は通常重要ではない。

== 高階ユニフィケーション ==
多くの用途で、一階の項ではなく[[型付きラムダ計算|型付きラムダ項]]のユニフィケーションを考慮する必要がある。そのようなユニフィケーションを「高階ユニフィケーション」と呼ぶことが多い。高階ユニフィケーションで特に研究が進んでいる領域は、αβη変換により単純な型付きラムダ項の等価性を判定する問題である。そのようなユニフィケーション問題は最大汎用単一子を持たない。高階ユニフィケーションは[[決定可能性|決定不能]]だが<ref>Warren Goldfarb:  [https://doi.org/10.1016/0304-3975(81)90040-2 The undecidability of the second-order unification problem]</ref><ref>[https://doi.org/10.1016/S0019-9958(73)90301-X Gérard Huet: The undecidability of unification in third order logic]</ref><ref>Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)</ref>、[[:en:Gérard Huet|Gérard Huet]] は単一子空間の体系的探索を可能にする[[帰納的可算集合|半決定可能]]なユニフィケーションアルゴリズム（Martelli-Montanari のユニフィケーションアルゴリズム<ref>[https://doi.org/10.1145/357162.357169 Martelli, Montanari: An Efficient Unification Algorithm]</ref>に高階の変数を含む項についての規則を加えて一般化したもの）を示した<ref>Gérard Huet: A Unification Algorithm for typed Lambda-Calculus []</ref>。Huet<ref>[http://portal.acm.org/citation.cfm?id=695200 Gérard Huet: Higher Order Unification 30 Years Later]</ref> と Gilles Dowek<ref>Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009-1062</ref> はこれに関する論文を書いている。

デール・ミラー<ref>{{lang-en-short|Dale Miller}}</ref>は高階パターン・ユニフィケーション<ref>{{lang-en-short|higher-order pattern unification}}</ref>と呼ばれるものを提案した<ref>Dale Miller: [http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/jlc91.pdf A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification], Journal of Logic and Computation, 1991, pp. 497--536</ref>。この高階ユニフィケーションのサブセットは決定可能であり、これで解けるユニフィケーション問題には最大汎用単一子が存在する。{{仮リンク|λProlog|en|λProlog||label=λ{{lang|en|Prolog}}}}や{{仮リンク|Twelf|en|Twelf|lang={{lang|en|Twelf}}}}といった高階の論理プログラミング言語は、完全な高階ユニフィケーションではなくパターン・ユニフィケーションを実装しているものが多い。

[[計算言語学]]では、[[省略]]法について最も有力な理論として、省略された要素を自由変数で表し高階ユニフィケーション (HOU) を使ってその値を決定するというものがある。例えば、ジョンはメアリーが好きで、ピーターも同様であるという文を like(j; m)R(p) のように意味論表現したとき、R（省略の意味論的表現）の値は like(j; m) = R(j) という等式で決定される。このような式を解くプロセスを高階ユニフィケーションと呼ぶ<ref>{{Citation |author=Claire Gardent, Michael Kohlhase, Karsten Konrad, |title= A multi-level, Higher-Order Unification approach to ellipsis |year=1997 | url= http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.9018}}</ref>。

== 一階の項の統語論的ユニフィケーションの例 ==
{{lang|en|Prolog}} では、大文字で始まるシンボルは変数名、小文字で始まるシンボルは関数名を表し、カンマは[[論理積]]として使われる。数学の慣習では小文字だけを使い、アルファベットの最後の方（たとえば <code>x,y,z</code>）は変数名、<code>f,g,h</code> といった文字は関数記号、<code>a,b,c</code> といった文字は定数を意味し、定数は引数を持たない関数とみなされる。論理積は <code>&amp;</code> または <math>\land</math> で表される。

{|class=wikitable
|-
!{{lang|en|Prolog}} の記法!!数学の記法!!ユニフィケーションに必要な置換!!備考
|-
|<code>a = a</code>||<math>a = a</math>||<math>\{\,\}</math> || 成功（[[恒真式]]）
|-
|<code>a = b</code>||<math>a = b</math>||失敗 || ''a'' と ''b'' は一致しない。
|-
|<code>X = X</code>||<math>x = x</math>||<math>\{\,\}</math> || 成功（[[恒真式]]）
|-
|<code>a = X</code>||<math>a = x</math>||<math>\{ x \mapsto a \}</math> || ''x'' は定数 ''a'' に単一化される。
|-
|<code>X = Y</code>||<math>x = y</math>||<math>\{ x \mapsto y \}</math> || ''x'' と ''y'' は別名である。
|-
|<code>f(a,X) = f(a,b)</code>||<math>f(a,x) = f(a,b)</math>||<math>\{ x \mapsto b \}</math> || 関数記号と定数記号が一致しているので、''x'' を 定数 ''b'' に単一化する。
|-
|<code>f(a) = g(a)</code>||<math>f(a) = g(a)</math>||失敗 || ''f'' と ''g'' は一致しない。
|-
|<code>f(X) = f(Y)</code>||<math>f(x) = f(y)</math>||<math>\{ x \mapsto y \}</math> || ''x'' と ''y'' は別名である。
|-
|<code>f(X) = g(Y)</code>||<math>f(x) = g(y)</math>||失敗 || ''f'' と ''g'' は一致しない。
|-
|<code>f(X) = f(Y,Z)</code>||<math>f(x) = f(y,z)</math>||失敗 || アリティが異なる。
|-
|<code>f(g(X)) = f(Y)</code>||<math>f(g(x)) = f(y)</math>||<math>\{ y \mapsto g(x) \}</math>|| ''y'' を項 ''g(x)'' に単一化する。
|-
|style=white-space:nowrap|<code>f(g(X),X) = f(Y,a)</code>||style=white-space:nowrap|<math>f(g(x),x) = f(y,a)</math>||<math>\{ x \mapsto a, y \mapsto g(a) \}</math>|| ''x'' を定数 ''a'' に、''y'' を項 ''g(a)'' に単一化する。
|-
|<code>X = f(X)</code>||<math>x = f(x)</math>||失敗とすべき || （{{仮リンク|出現検査|en|occurs check}}により）厳密な一階述語論理では失敗となり、最近のPrologでも失敗する。古い実装のPrologでは ''x'' が ''x=f(f(f(f(...))))'' という無限の式に単一化されるが、これは厳密には項ではない。
|-
|<code>X = Y, Y = a</code>||<math>x = y \land y = a</math>||<math>\{ x \mapsto a, y \mapsto a \}</math>|| ''x'' と ''y'' が共に定数 ''a'' に単一化される。
|-
|<code>a = Y, X = Y</code>||<math>a = y \land x = y</math>||<math>\{ x \mapsto a, y \mapsto a \}</math>|| 同上（ユニフィケーションは[[対称関係|対称的]]で[[推移関係|推移的]]である）
|-
|<code>X = a, b = X</code>||<math>x = a \land b = x</math>||失敗 || ''a'' と ''b'' は一致しないので、''x'' はどちらとも単一化できない。
|}

== アルゴリズム ==
項 <math>s_0,t_0, \ldots, s_n,t_n</math> についてのユニフィケーション問題 <math>G</math> が <math>\text{ } G = \{ s_1 \stackrel{\text{?}}{=} t_1, \ldots , s_n \stackrel{\text{?}}{=} t_n \}</math> という潜在的等式の[[多重集合]]で表されるとき、そのアルゴリズムはそれらの式に以下に示す項書き換え規則を適用し、等価な形式である <math>\{ x_1 \stackrel{\text{?}}{=} u_1, \ldots, x_m \stackrel{\text{?}}{=} u_m \}</math> に変形しようとする。ここで、<math>x_0,\ldots,x_m</math> は一意な変数である（1つの式の左辺に一度だけ現れ、他の部分には出現しない）。この形式の多重集合は置換を表しているとみなすことができる。解がない場合、アルゴリズムは <math>\bot</math> とともに停止する。項 <math>t</math> に含まれる変数群を <math>Vars(t)</math> と表記し、問題 <math>G</math> 内の式の左辺と右辺の全ての項に含まれる変数の集合は <math>Vars(G)</math> と表記する。問題 <math>G</math> 内での変数 <math>x</math> の出現を全て項 <math>t</math> に置換することを <math>G\{ x \mapsto t\}</math> と表記する。簡単にするため、定数記号は引数ゼロ個の関数記号とみなす。

<math>G \cup \{ t \stackrel{\text{?}}{=} t \} \Rightarrow G</math>

<math>G \cup \{ f(s_1,\dots,s_k) \stackrel{\text{?}}{=} f(t_1,\ldots,t_k) \} \Rightarrow G \cup \{ s_1 \stackrel{\text{?}}{=} t_1, \ldots, s_k \stackrel{\text{?}}{=} t_k \}</math>

<math>G \cup \{ f(s_1,\dots,s_k) \stackrel{\text{?}}{=} g(t_1,\ldots,t_m) \} \Rightarrow \bot \text{  if } f \neq g \lor k \neq m</math>

<math>G \cup \{ f(s_1,\dots,s_k) \stackrel{\text{?}}{=} x \} \Rightarrow G \cup \{ x \stackrel{\text{?}}{=} f(s_1,\dots,s_k) \}</math>

<math>G \cup \{ x \stackrel{\text{?}}{=} t \} \Rightarrow G\{ x \mapsto t \} \cup \{ x \stackrel{\text{?}}{=} t \}
 \text{  if } x \in Vars(G) \land x \notin Vars(t)</math>

<math>G \cup \{ x \stackrel{\text{?}}{=} f(s_1,\dots,s_k) \} \Rightarrow \bot \text{  if } x \in Vars(f(s_1,\dots,s_k))</math>

=== 停止することの証明 ===
停止性の証明においては <NUVN,NLHS,EQN> という3タプルを考察する。NVUN は一意でない変数の数<ref>{{lang-en-short|number of non-unique variables}}</ref>、NLHS は潜在的等式の左辺にある関数記号と定数の数<ref>{{lang-en-short|number of function symbols and constants on the LHS of potential equations}}</ref>、EQN は等式の数<ref>{{lang-en-short|number of equations}}</ref>である。書き換え規則をどのような順序で適用しても、書き換えの度にNUVNは減るか、減らずに現状維持するかのどちらかなので、最終的に停止する。NUVNが現状維持した場合、NLHSが書き換えによって減るか、減らずに現状維持するかのどちらかである。NUVNとNLHSがどちらも現状維持した場合、EQNが書き換えによって減る。

==== 構造上再帰的なユニフィケーション ====
{{仮リンク|コナー・マクブリッジ|en|Conor McBride}}は、{{仮リンク|Epigram (プログラミング言語)|en|Epigram (programming language)|label=Epigram}}のような{{仮リンク|依存型 (型理論)|en|Dependent type|label=依存型}}言語で「ユニフィケーションが利用している構造を表現することにより」、ジョン・アラン・ロビンソンのアルゴリズムを再帰的にすることができ、証明の複数の停止条件は不要になることを示した<ref>{{Cite journal |last=McBride |first=Conor |title=First-Order Unification by Structural Recursion |journal=Journal of Functional Programming |year=2003 |month=October |volume=13 |issue=6 |pages=1061–1076 |doi=10.1017/S0956796803004957 |url= http://strictlypositive.org/unify.ps.gz |accessdate=2012-03-30 |issn=0956-7968}}</ref>。

== 脚注 ==
{{Reflist}}

== 関連項目 ==
* [[反ユニフィケーション]]

== 参考文献 ==
* F. Baader and T. Nipkow, ''[https://web.archive.org/web/20051120123456/http://www4.informatik.tu-muenchen.de/~nipkow/TRaAT/ ''Term Rewriting and All That''].'' Cambridge University Press, 1998.
* F. Baader and W. Snyder,  ''[http://lat.inf.tu-dresden.de/research/papers/2001/BaaderSnyderHandbook.ps.gz ''Unification Theory''].'' In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers, 2001.
* [[ジョセフ・ゴーグエン|Joseph Goguen]], ''[http://www-cse.ucsd.edu/~goguen/projs/sem.html ''What is Unification?''].''
* {{MathWorld | urlname=Unification | title=Unification | author=Alex Sakharov}}

{{DEFAULTSORT:ゆにふいけしよん}}
[[Category:ユニフィケーション|*]]
[[Category:計算機科学における論理]]
[[Category:形式手法]]
[[Category:数学に関する記事]]
[[Category:論理プログラミング]]
[[Category:自動定理証明]]