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í.

Zdroj