Unifikacja – proces algorytmiczny, za pomocą którego można próbować rozwiązać problem spełnialności. Celem unifikacji jest znalezienie warunku zastępczego, który pokazuje, że dwa warunki pozornie różne są w rzeczywistości albo identyczne, albo po prostu równe. Unifikacja jest szeroko stosowana w rozumowaniu automatycznym, programowaniu logicznym i wdrażaniu języków programowania.

Bibliografia

• Franz Baader, Tobias Nipkow: Term Rewriting and All That. Cambridge University Press, 1998. ISBN 978-0521779203. (ang.).brak strony w książce
• Franz Baader, Wayne Snyder: Unification Theory. W: John Alan Robinson, Andrei Voronkov: Handbook of Automated Reasoning. T. I. Elsevier Science Publishers, 2001-06, s. 447–533. ISBN 978-0-444-50813-3. (ang.).