Unifikace (logika)

Unifikace je v logice substituce, po jejíž aplikaci na množinu termů dostaneme jeden term. Formálně, je-li $𝒯\mathcal{(}ℱ,𝒱\mathcal{)}$ algebra termů a t a s dva termy, je substituce $\sigma$ jejich unifikací, pokud $t\sigma =s\sigma$. Algoritmus unifikace termů predikátové logiky byl poprvé formulován Alanem Robinsonem v roce 1965 a použit pro rezoluci v predikátové logice. Používá se například v unifikačních gramatikách.

Sémantická unifikace

Sémantická unifikace je zobecněním syntaktické. Pracuje s rovnostmi nad termy a hledá takové substituce, jež unifikují term vzhledem k nějaké teorii rovnic. Máme-li například teorii $E=\{f(x,y)\approx f(y,x)\}$ a unifikační problém $\mathrm{\Gamma }=\{f(x,y)\stackrel{?}{=}f(a,b)\}$ (resp. $E\models f(x,y)=f(a,b)$), jsou řešením substituce $\{x\mapsto a,y\mapsto b\}$ a $\{x\mapsto b,y\mapsto a\}$. Jak je vidět, na rozdíl od syntaktické unifikace může mít sémantická unifikace více na sobě nezávislých řešení.

Externí odkazy

• Šablona:Commonscat