Group Embeddings of Configurations with Prover9
Eric Ens and R. Padmanabhan

A configuration is a finite set of elements (called "points" just to have a
guiding analogy with the plane geometry) and a finite set of blocks (again, we
call them "lines") such that each point is incident with the same number of
lines and each line is incident with same number of points. The most well-known
examples of configurations are the 7-point Fano configuration, the 9-point
configuration of inflection points on a complex cubic and the 10-point
Desargues configuration. This topic was popularized by Hilbert and Cohn-Vossen
in their celebrated book Anschauliche Geometry (reprinted in English as
Geometry and Imagination). Motivated by the geometric definition of a group law
on non-singular cubic curves, we define the concept of group embeddability of
(n, k) configurations and classify the set of all (11, 3) s which can be
embedded into abelian groups in such a way that if {P,Q,R} is a line in the
configuration then P+Q+R = 0 in the abelian group. We apply these results to
their geometric realizability (over a projective plane). Naturally, there are
two kinds of theorems we need to prove: for a given configuration, we have
either a concrete group representation or else a proof that no such
representation exists. Prover9 is successfully employed to get the proofs of
both kinds.