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 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á 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 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í.