A Decision Procedure for Equational Reasoning in Commutative Algebraic Structures
Luı́s Cruz-Filipe, Freek Wiedijk · 2004
Abstract. We present a decision procedure for equational reasoning in abelian groups, commutative rings and fields that checks whether a given equality can be proven from the axioms of these structures. This has been implemented as a tactic in Coq; here we give a mathematical description of the decision procedure that abstracts from Coq specifics, making the work in principle adaptable to other theorem provers. Within Coq we prove that this decision procedure is correct. On the meta-level we analyse its completeness, showing that it is complete for groups and rings in the sense that the tactic succeeds in finding a proof of an equality if and only if that equality is provable from the group/ring axioms without any hypotheses. Finally we characterize in what way our method is incomplete for fields.