Unifikation

Fra latin: unificere = gøre til ét, forene, sammensætte.

I logikprogrammering er unifikation en central metode. Formålet med unifikation er at forene to grupper af udsagn mv. til én.

På et teknisk niveau betyder det, at termer (konstanter, variable eller funktorer/prædikater med argumenter) skal forenes parvis. På et højere niveau spiller unifikation en rolle i problemløsning som (1) en metode til at kombinere brugbar viden med relevans for det nærværende problem, som er omfattende nok til at løse eller dekomponere det til delproblemer; eller (2) at specialisere både viden og problemet sådan, at de passer sammen.

Inferensmaskinen integrerer resultatet af unifikationen og resten af systemets viden.