Unifikace (logika)

Z Wikipedie, otevřené encyklopedie
Skočit na: Navigace, Hledání

Unifikace je v logice substituce, po jejíž aplikaci na množinu termů dostaneme jeden term. Formálně, je-li \mathcal{T(F,V)} 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.

Sémantická unifikace[editovat | editovat zdroj]

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 \Gamma=\{f(x,y)\overset{?}{=}f(a,b)\} (resp. E\vDash 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í.