Unifikacja (logika)

Unifikacja w informatyce i logice - 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

1. F. Baader, T. Nipkow: Term Rewriting and All That. Cambridge University Press, 1998. 
2. F. Baader, W. Snyder: Unification Theory. W: J.A. Robinson, A. Voronkov: Handbook of Automated Reasoning. T. I. Elsevier Science Publishers, 2001, s. 447-533.