Redigerer Unifikasjon (avsnitt)

==Eksempler på unifikasjon==

''I Prolog, av konvensjon, begynner atomer med små bokstaver.''

* ''A'', ''A'' : Unifikasjon lykkes ([[Tautologi (logikk)|tautologi]])
* ''A'', ''B'', ''abc'' : Både ''A'' og ''B'' unifiseres med atomet ''abc''
* ''abc'', ''B'', ''A'' : Som over (unifikasjon er symmetrisk)
* ''abc'', ''abc'' : Unifikasjon lykkes, like atomer
* ''abc'', ''xyz'' : Unifikasjon feiler, kan ikke unifisere ulike atomer
* ''f''(''A''), ''f''(''B'') : ''A'' unifiseres med ''B''
* ''f''(''A''), ''g''(''B'') : Unifikasjon feiler, ulike funksjoner så termer er ulike
* ''f''(''A''), ''f''(''B'', ''C'') : Unifikasjon feiler, termer har ulik aritet
* ''f''(''g''(''A'')), ''f''(''B'') : Unifiserer ''B'' med termen ''g''(''A'')
* ''f''(''g''(''A''), ''A''), ''f''(''B'', ''xyz'') : Unifiserer ''A'' med atomet ''xyz'' og ''B'' med termen ''g''(''xyz'')
* ''A'', ''f''(''A'') : Uendelig unifikasjon, ''A'' unifiseres med ''f''(''f''(''f''(''f''(...)))). I første ordens logikk og i mange moderne Prolog dialekter er dette ulovlig (og hindres av ''[[forekomst sjekken]]'')
* ''A'', ''abc'', ''xyz'', ''X'': Unifikasjon feiler, finnes ingen unifikasjon som gjør ''A'' = ''abc'' =''X'' = ''xyz''