Automated reasoning about cubic curves

It is well known that the n-ary morphisms defined on projective algebraic curves satisfy some strong local-to-global equational rules of derivation not satisfied in general by universal algebras. For example, every rationally defined group law on a cubic curve must be commutative. Here, we extract from the geometry of curves a first-order property (gL) satisfied by all morphisms defined on these curves such that the equational consequences known for projective curves can be derived automatically from a set of six rules (stated within the first-order logic with equality). First, the rule (gL) is implemented in the theorem-proving program . Then, we use to automatically prove some incidence theorems on projective curves without any further reference to the underlying geometry or topology of the curves.