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

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

potom platí 

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

Matematická logika