Unifikace (logika)

Unifikace je v logice substituce, po jejíž aplikaci na množinu termů dostaneme jeden term. Formálně, je-li ${\displaystyle {\mathcal {T(F,V)}}}$ algebra termů a t a s dva termy, je substituce ${\displaystyle \sigma }$ jejich unifikací, pokud ${\displaystyle 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 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 ${\displaystyle E=\{f(x,y)\approx f(y,x)\}}$ a unifikační problém ${\displaystyle \Gamma =\{f(x,y){\overset {?}{=}}f(a,b)\}}$ (resp. ${\displaystyle E\vDash f(x,y)=f(a,b)}$), jsou řešením substituce ${\displaystyle \{x\mapsto a,y\mapsto b\}}$ a ${\displaystyle \{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í.

• Obrázky, zvuky či videa k tématu unifikace na Wikimedia Commons