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

Kategorie:Matematická logika