Unifikace literálů

Chceme-li rezolvovat klauzule, brání nám to, že termy/argumenty nejsou stejné. Všechny proměnné jsou ale kvantifikovány všeobecným kvantifikátorem, a tudíž můžeme použít zákon konkretizace a pokusit se najít vhodnou substituci termů za proměnné tak, abychom dostali shodné „unifikované” literály. Je-li term substituovatelný za  ve formuli , pak .