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:


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.out 
Theorem 3:
    otter -f > thm3.out 
Theorem 4:
    otter -f > thm4.out 
Lemma 1:
    otter -f > lem1.out 
Lemma 2:
    otter -f > lem2.out 
Theorem 5:
    otter -f > thm5.out 
Theorem 7:
    otter -f > thm7.out 
Theorem 8:
    otter -f > thm8.out 
Counterexample to weakened form of Theorem 8:
    mace2 -n3 -p > mace8.out