This Web page support the following paper.

# Uniqueness of Steiner Laws on Cubic Curves

## R. Padmanabhan and W. McCune

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.

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
```