http://profs.sci.univr.it/~farinelli/courses/ar/slides/paramodulation.pdf 自動定理証明で等号を扱うための推論規則であるParamodulationについての、分かりやすい説明。