Editing Occurs check (section)

==Application in theorem proving==

In [[theorem proving]], unification without the occurs check can lead to [[soundness|unsound]] [[inference]]. For example, the [[Prolog]] goal
<math>X = f(X)</math>
will succeed, binding ''X'' to a cyclic structure which has no counterpart in the [[Herbrand universe]].
As another example,<ref>{{cite book| author=David A. Duffy| title=Principles of Automated Theorem Proving| year=1991| publisher=Wiley}}; here: p.143</ref>
without occurs-check, a [[Resolution (logic)|resolution proof]] can be found for the non-theorem<ref>Informally, and taking <math>p(x,y)</math> to mean e.g. "''x loves y''", the formula reads "''If everybody loves somebody, then a single person must exist that is loved by everyone.''"</ref>
<math>(\forall x \exists y. p(x,y)) \rightarrow (\exists y \forall x. p(x,y))</math>: the negation of that formula has the [[conjunctive normal form]] <math>p(X,f(X)) \land \lnot p(g(Y),Y)</math>, with <math>f</math> and <math>g</math> denoting the [[Skolem function]] for the first and second existential quantifier, respectively. Without occurs check, the literals <math>p(X,f(X))</math> and <math>p(g(Y),Y)</math> are unifiable, producing the refuting empty clause.

[[File:Example for syntactic unification without occurs check leading to infinite tree svg.svg|thumb|upright=0.75|Cycle by omitted occurs check]]