unifikáció
Unifikáció, vagy unification, a logika és a számítástechnika területén a két kifejezés összeegyeztethetőségének keresését jelenti. A kifejezések általában változókból, konstansokból és függvényjelekből álló fastruktúrák. Egy helyettesítés (substitution) megadja, hogy a változókat milyen kifejezésekkel kell felváltani. Két kifejezés akkor egyeztethető össze, ha létezik olyan helyettesítés, amely alkalmazva mindkét oldalon egyenlő kifejezést ad.
Az unifikáció célja egy olyan legáltalánosabb helyettesítés megtalálása, amely az egyik oldalon és a másikon alkalmazva
Robinson elsőrendű unifikációs algoritmusa meghatározza, hogy két elsőrendű kifejezésre létezik-e MGU, és ha igen, azt megadja.
Alkalmazások: logikai programozás (például Prolog), automatikus bizonyítás, típusinferencia a funkcionális nyelvekben (Hindley–Milner), szimbolikus számítás és természetes
Variánsok közé tartozik az AC-unifikáció (asszociatív- és kommutatív elvek figyelembe vétele) és a higher-order unifikáció (lambda-kifejezésekre).