Automated reasoning about cubic curves (Q1343392)

This papers provides automated reasoning about incidence theorems on projective curves without referring for geometry or topology of the curves. For this purpose, a first-order property is extracted from the geometry of curves, and implemented in the computer program OTTER for proving theorems stated in first-order logic with equality. The computer program is available by electronic mail to otter\(\@\)mcs.anl.gov.