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.

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