Paramodulace

Paramodulace je technika používaná v automatickém dokazování tvrzení. Pokud

$A=B,C=D$

a C se unifikuje s podtermem A na pozici p, tj. existuje substituce $\sigma$ taková, že

$\sigma A_p=\sigma C$

potom platí

$\sigma A[D{]}_p=\sigma B$

Ve spojení s principem rezoluce je tak možné hledat důkazy tvrzení v predikátové logice s rovností.