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.
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
Input and Output Files
otter -f thm2.in > thm2.out
otter -f thm3.in > thm3.out
otter -f thm4.in > thm4.out
otter -f lem1.in > lem1.out
otter -f lem2.in > lem2.out
otter -f thm5.in > thm5.out
otter -f thm7.in > thm7.out
otter -f thm8.in > thm8.out
Counterexample to weakened form of Theorem 8:
mace2 -n3 -p mace8.in > mace8.out