Разбира се, за да имат две атомарни формули най-общ унификатор, необходимо е те да са унифицируеми. Ще докажем, че това необходимо условие е и достатъчно. Нека φ и ψ са две унифицируеми атомарни формули, Ще покажем, че те имат най-общ унификатор, който при това е идемпотентен и действа в обединението на VAR(φ) и VAR(ψ). Ако φ и ψ са една и съща формула, то такъв техен най-общ унификатор очевидно е тъждествената субституция. Затова да предположим, че атомарните формули φ и ψ са различни. Тогава, както знаем, може да се образува нетъждествена система от уравнения между термове, решения на която са точно унификаторите на φ и ψ. Поради това, че φ и ψ са унифицируеми, тя ще има идемпотентно най-общо решение, което действа в множеството на нейните променливи (то може да се намери по метода, разгледан във въпроса „Решаване на системи от уравнения между термове“). Това решение е най-общ унификатор на φ и ψ със споменатите допълнителни свойства.

    Пример 1. При сигнатура с константи a и b и двуместен предикатен символ p унификатори на атомарните формули  p(a,Y) и  p(X,b) са точно онези субституции, които са решения на системата

    Пример 2. При сигнатура с едноместен функционален символ f и двуместен предикатен символ p унификатори на атомарните формули  p(X,f(X)) и  p(f(Y),Z) са точно онези субституции, които са решения на системата

    Пример 3. При сигнатура с константа a, едноместен функционален символ f и двуместен предикатен символ p унификатори на атомарните формули  p(X,f(Y)) и  p(f(a),X) са точно онези субституции, които са решения на системата

    Забележка 1.Най-общият унификатор на две атомарни формули, когато съществува, не е единствен. И наистина, нека σ е най-общ унификатор на две атомарни формули φ и ψ. Ще покажем, че при всеки избор на две различни променливи ζ₁ и ζ₂ произведението σ[ζ₁/ζ₂,ζ₂/ζ₁] също е най-общ унификатор на φ и ψ. При произволно избрани различни променливи ζ₁ и ζ₂ да означим споменатото произведение с σ′. Това, че то е унификатор на φ и ψ, е ясно, защото то е частен случай на σ. Наред с това обаче благодарение на лесно проверимото равенство [ζ₁/ζ₂,ζ₂/ζ₁][ζ₁/ζ₂,ζ₂/ζ₁] = ι може да се твърди, че σ = σ′[ζ₁/ζ₂,ζ₂/ζ₁], а това позволява да заключим, че всеки частен случай на σ е частен случай и на σ′, следователно всеки унификатор на φ и ψ е частен случай и на σ′. От друга страна не е трудно ζ₁ и ζ₂ да се изберат по такъв начин, че субституцията σ′ да бъде различна от σ. За да се убедим в това, достатъчно е да изберем ζ₁ така, че да е в сила равенството  ζ₁σ = ζ₁, и да сравним резултатите от прилагането на двете субституции към променливата ζ₁.

    Забележка 2. Когато две атомарни формули са унифицируеми, измежду унификаторите им сигурно има такива, които не са най-общи. Действително, нека една субституция σ е унификатор на две дадени атомарни формули φ и ψ. Да си вземем две различни променливи ζ₁ и ζ₂, такива, че  ζ₁σ = ζ₁ и  ζ₂σ = ζ₂, и да означим със σ′ субституцията σ[ζ₂/ζ₁]. Тогава σ′ пак е унификатор на φ и ψ, защото е частен случай на техния унификатор σ, но за разлика от него преобразува променливите ζ₁ и ζ₂ в един и същ терм (а именно в променливата ζ₁). Лесно е да се убедим, че и всяка субституция, която е частен случай на σ′, също ще преобразува ζ₁ и ζ₂ в един и същ терм. Поради това субституцията σ не е частен случай на σ′ и значи σ′ не е най-общ унификатор на φ и ψ.

    Забележка 3. За някои две унифицируеми атомарни формули φ и ψ може да се случи всички унификатори (най-общи или не) да съвпадат върху обединението на множествата VAR(φ) и VAR(ψ). Положението е такова точно тогава, когато е налице най-общ унификатор на φ и ψ, съпоставящ на всички променливи от споменатото обединение затворени термове (както е в примери 1 и 3 по-горе).

Последно изменение: 1.07.2008 г.