This Web page support the following paper.

Uniqueness of Steiner Laws on Cubic Curves

This Web page support a paper of the same name to appear shortly.

Final Version:

## Abstract

It is well known that projective curves admit at most one group law.
In particular, the familiar group law on a nonsingular cubic is
unique up to isomorphism. In this paper we show that such curves
admit a unique Stenier law. Our proofs are strictly first-order and
employ automated deduction by transforming certain incidence theorems
into formal implications. Besides being elementary, this provides a
variety of examples for computer scientists designing theorem provers
and gives new insights and interpretations for the various synthetic
geometric constructions.
## Programs

Otter
and
Mace2.
## Input and Output Files

Theorem 2:
otter -f thm2.in > thm2.out

Theorem 3:
otter -f thm3.in > thm3.out

Theorem 4:
otter -f thm4.in > thm4.out

Lemma 1:
otter -f lem1.in > lem1.out

Lemma 2:
otter -f lem2.in > lem2.out

Theorem 5:
otter -f thm5.in > thm5.out

Theorem 7:
otter -f thm7.in > thm7.out

Theorem 8:
otter -f thm8.in > thm8.out

Counterexample to weakened form of Theorem 8:
mace2 -n3 -p mace8.in > mace8.out