Proving Theorems with the Modification Method
Daniël Brand · SIAM Journal on Computing · 1975
A method for proving theorems in first order predicate calculus theories with equality is described and proven complete. Completeness of this “Modification Method” implies completeness of Paramodulation without the functionally reflexive axioms, thus proving a conjecture of Wos and Robinson (1969). Moreover, completeness holds with some other restrictions, such as limiting paramodulation into variables. Experimental results using the Modification Method are included.