Přeskočit na obsah

Paramodulace

Z Wikipedie, otevřené encyklopedie

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