Unifikace (logika)

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. 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. +more 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í.

Externí odkazy

Kategorie:Logika