Otevřít hlavní menu

Unifikace je v logice substituce, po jejíž aplikaci na množinu termů dostaneme jeden term. Formálně, je-li algebra termů a t a s dva termy, je substituce jejich unifikací, pokud . 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á unifikaceEditovat

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   a unifikační problém   (resp.  ), jsou řešením substituce   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í.