Single axioms for the left group and right group calculi.
William W. McCune · Notre Dame Journal of Formal Logic · 1992
This article is on axiomatizations of the left group calculus and of the right group calculus.The axiomatizations use modus ponens rather than equality substitution as the inference rule.The structures being axiomatized are ordinary free groups, and the sole operation is division.Previous axiomatizations are due to J. A. Kalman.The article contains single axioms and other simple axiomatizations of the two calculi.An automated theoremproving program was used extensively to find candidate axiomatizations and to find proofs that candidates are in fact axiomatizations.