Paramodulacja to algorytm automatycznego dowodzenia twierdzeń w systemach z równością.
Paramodulacja z grubsza polega na tym, że:
- jeśli oraz to
Mówiąc zaś bardziej formalnie, jeśli i unifikuje się z podtermem na pozycji to gdzie to unifikator i
- Przykład
Unifikujemy w z
Unifikator to Zastępujemy więc przez
wszystkie wystąpienia zmiennych i zastępujemy zgodnie z unifikatorem.
W wyniku otrzymujemy