These web pages are a supplement to the following paper.

# Computer and Human Reasoning: Single Implicative Axioms for Groups and for Abelian Groups

## W. McCune and A.D.Sands

The paper appears in American Mathematical Monthly 103(10):888-892 (December 1996). Here is a preprint.

## Abstract

The paper presents single implicative axioms for abelian groups in terms of addition and inverse and in terms of subtraction, and implicative single axioms for (ordinary) groups in terms of product and inverse and in terms of division. Two of the axioms were found by a human, and the other two by computer. The proofs in the paper are adapted from proofs found by the automated deduction system Otter.

## Theorems in the Paper

• Theorem 1.    x+y = z+u  ->  (y´+z)+u = x
is a single axiom, in terms of addition and inverse, for abelian groups.
• Theorem 2.    x-y = z-u  ->  u-(z-x) = y
is a single axiom, in terms of subtraction, for abelian groups.
• Theorem 3.    (x·y)·z = (x·u)·w  ->  u·(w·z´) = y
is a single axiom, in terms of product and inverse, for group theory.
• Theorem 4.    x/y=z/u  ->  y/(((z/z)/z)/((x/x)/x))=u
is a single axiom, in terms division, for group theory.