Ако в системата (1) някое от уравненията няма решение, то очевидно и цялата система няма решение. Сега ще отбележим изрично два случая, когато уравнение, на което страните са термове, няма решение; ще ги наричаме съответно първи и втори случай на явна нерешимост, а всяко уравнение, за което е налице някой от тези два случая, ще наричаме явно нерешимо. Първият случай е онзи, когато никоя от двете страни на уравнението не е променлива и двете страни не са еднотипни. Такова уравнение няма решение, защото при прилагане на произволна субституция към двете страни на уравнението, получаваме пак уравнение с тези свойства. Вторият случай е налице за уравненията от вида ξ = θ, където ξ е променлива, θ е терм, който не е променлива, и ξ е променлива на θ. Уравнение от такъв вид няма решение поради факта, че при изказаните предположения за ξ и θ дължината на терма θσ ще бъде строго по-голяма от дължината на терма ξσ, както и да избираме субституцията σ (въпросният факт се установява като най-напред се докаже индуктивно за произволен терм θ условното твърдение, че ако ξ е променлива на θ, то дължината на θσ е не по-малка от дължината на ξσ, а след това се покаже, че неравенството между двете дължини е строго при допълнителното условие термът θ да не е променлива).

    Забележка 1. Всяка софтуерна реализация на Пролог използва съществено някой метод за унификация, а при коректното му използване би трябвало унификацията да е невъзможна, когато при опит за нейното осъществяване възникне някой от отбелязаните два случая на явна нерешимост. В някои от реализациите на Пролог обаче (но не и в Strawberry Prolog) съзнателно е допусната некоректност на действията при възникване на втория от тези случаи, като заради повишаване на бързодействието е спестен тъй нареченият „occurs check“.

    Ако в една система от вида (1) поне едно от уравненията е явно нерешимо, то и за самата система ще казваме, че е явно нерешима.

    Система в решен вид ще наричаме всяка система уравнения от вида (1), в която τ₁, …, τ_n са различни помежду си променливи, които не са променливи на никой от термовете θ₁, …, θ_n. Ще покажем, че ако (1) е система в решен вид, a σ° е субституцията

(2)

[τ1/θ1,…,τn/θn],

то σ° е решение на системата (1) и за всяко решение σ на тази система е в сила равенството  σ = σ°σ . За целта да предположим, че е изпълнена предпоставката на това твърдение. Благодарение на обстоятелството, че τ_i не е променлива на θ_j при i,j=1,…,n, може да се твърди, че субституцията σ° съвпада с тъждествената субституция върху всяко от множествата VAR(θ_j), j=1,…,n, следователно θ_jσ° = θ_j, j=1,…,n. Като вземем пред вид и равенствата τ_jσ° = θ_j, j=1,…,n, виждаме, че σ° е решение на системата (1). Нека сега σ да бъде произволно решение на същата система, т.е. нека да са в сила равенствата τ_jσ = θ_jσ, j=1,…,n. Ще покажем, че субституциите σ и σ°σ съвпадат за всяка променлива. И наистина, нека ξ е произволна променлива. Ако тя е променливата τ_j за някое j от множеството {1,…,n}, то имаме

    Забележка 2. Да се условим да казваме, че дадена субституция действа в дадено множество от променливи, ако на променливите от това множество тя съпоставя термове, чиито променливи са от същото множество, а на всяка друга променлива съпоставя самата нея. Под множество на променливите на една система от уравнения между термове ще разбираме обединението на множествата на променливите на левите и на десните страни на уравненията й. Очевидно е, че когато (1) е система от уравнения между термове, която е в решен вид, съответната субституция (2) действа в множеството на променливите на (1).

    Забележка 3. Най-общо решение на една система от уравнения между термове се нарича такова нейно решение, че всяко от решенията й е негов частен случай (т.е. може да се получи от него чрез умножаване отдясно с подходяща субституция). Ако разполагаме с най-общо решение на такава система, можем лесно да опишем кои са всички нейни решения  –  те ще бъдат точно неговите частни случаи (това следва от дефиницията за най-общо решение и от обстоятелството, че, както лесно се вижда, всеки частен случай на решение на системата е пак нейно решение). От доказаното по-горе е ясно, че ако (1) е система от уравнения между термове, която е в решен вид, то субституцията (2) е нейно най-общо решение. Като приложим равенството  σ = σ°σ  със σ° в качеството на σ, виждаме още, че тази субституция е равна на произведението си със самата нея. Субституциите с това свойство се наричат идемпотентни. Една система от уравнения между термове, която е в решен вид, може да има и неидемпотентно най-общо решение, действащо в множеството на нейните променливи. Такъв е случаят например със системата, състояща се само от уравнението

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