Z-module reasoning
Tie-Cheng Wang · Journal of the ACM · 1993
A Z-module reasoning method has been formulated for equality-oriented theoremproving in basic ring theories.This method incorporates equality theory and a set of basic axioms of rings into inference rules based on linearization, identity paramodulation, and integer Gaussimr elimination.Z-module reasoning proves a theorem by means of two distinct types of reasoning.One type of reasoning employs paramodulation-based deduction to deduce a set of identity vectors from a denial of the theorem.The other type of reasomng employs integer array manipulation to calculate the truth of the theorem in terms of the Z-module generated by these vectors.This paper is devoted to a formal description of Z-module reasoning, including motivation and background, formal defimtion, soundness and completeness theorems, the finite hnearization property on standard polynomial sets, and the existence of a decisional Z-module reasoning prover for homogeneous equational sets.The relation of Z-module reasoning with other work and issues concerning the refinements and future research of the method E also discussed.