ユニフィケーション
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/09 03:08 UTC 版)
ユニフィケーション（英: unification）は数理論理学や計算機科学の用語であり、充足性問題を解く際のアルゴリズム的プロセスである。ユニフィケーションは、見た目の異なる2つの項が同一[1]または同等[2]であることを示す置換を求めるのが目的である。ユニフィケーションは自動推論、論理プログラミング、プログラミング言語の型システムの実装などに幅広く用いられている。
- ^ 英: identical
- ^ 英: equal
- ^ 英: syntactic unification
- ^ 英: equality
- ^ 英: semantic unification
- ^ 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.
- ^ Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009). Lectures on Jacques Herbrand as a Logician (SEKI Report). arXiv:0902.4682. Here: p.56
- ^ Jacques Herbrand (1930). Recherches sur la théorie de la demonstration (PDF) (Ph.D. thesis). A. 1252. Université de Paris. Here: p.96-97
- ^ 英: occurs check
- ^ 英: unifier
- ^ a b 英: most general unifier
- ^ 英: equational-unification。e-unification とも呼ばれる。
- ^ lamdaPrologなど
- ^ Russell, Norvig: Artificial Intelligence, A Modern Approach, p. 277
- ^ Warren Goldfarb: The undecidability of the second-order unification problem
- ^ Gérard Huet: The undecidability of unification in third order logic
- ^ Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)
- ^ Martelli, Montanari: An Efficient Unification Algorithm
- ^ Gérard Huet: A Unification Algorithm for typed Lambda-Calculus []
- ^ Gérard Huet: Higher Order Unification 30 Years Later
- ^ Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009-1062
- ^ 英: Dale Miller
- ^ 英: higher-order pattern unification
- ^ Dale Miller: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, 1991, pp. 497--536
- ^ Claire Gardent, Michael Kohlhase, Karsten Konrad, (1997), A multi-level, Higher-Order Unification approach to ellipsis
- ^ 英: number of non-unique variables
- ^ 英: number of function symbols and constants on the LHS of potential equations
- ^ 英: number of equations
- ^ McBride, Conor (October 2003). “First-Order Unification by Structural Recursion”. Journal of Functional Programming 13 (6): 1061–1076. doi:10.1017/S0956796803004957. ISSN 0956-7968 2012年3月30日閲覧。.
[続きの解説]
「ユニフィケーション」の続きの解説一覧
- ユニフィケーションのページへのリンク
