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.


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

Otter Input Files and Proofs