Talk:Unification

From Wikipedia, the free encyclopedia

Should this page be renamed, e.g., Unification (Prolog) or Unification (Computer Programming)? --Nate

No; this is essentially the same concept as is used in various theorem provers and type checkers, and is not specific to Prolog or to computer programming. (Although in most "mathematical" uses of unification, the example A=f(A) fails rather than returning an infinite term; the extra step in the unification algorithm which checks for this case and makes it fail is called the "occurs check".) Carl

I agree. This means that the dominance of Prolog should somehow be removed from the article. The right context to mention is First-order resolution; note that Prolog uses just a particular form of resolution. Higher-order unification should also be mentioned. --Tillmo 03:57, 24 August 2005 (UTC)

We really ought to distinguish between syntactic unification (discussed here) and E-unification (not yet discussed). E-unification is really important in automated theorem proving. Syntactic unification (and matching) also has important applications aside from Prolog; in ML-style languages, for instance. Perhaps some discussion of the problem of coverage analysis would also be useful?--Iwehrman 17:01, 27 Mar 2005 (UTC)

[edit] link to non-compsci logic unification would be dandy

I've no luck finding a page on this kind of unification that doesn't assume the reader wants to do it in Prolog/Lisp/etc. If there are any good web pages that explain unification on logic with a series of clauses containing nothing but plain ol' variables (not even quantifiers, just variables) as you would do logic problems on paper, I think a link to that would be useful. --I am not good at running 21:32, 23 October 2005 (UTC)