No label defined (Q4946223)

The authors propose, in the case of plane projective geometry, an alternative to the algebraic approaches to mechanical geometry theorem proving (such as those in \textit{S.-C. Chou} [Mechanical geometry theorem proving (D. Reidel, Dordrecht-Boston) (1988; Zbl 0661.14037)] or \textit{W. T. Wu} [Mechanical theorem proving in geometries (Springer-Verlag, Berlin) (1994; Zbl 0831.03003)]). It is based on equational matrices of incidence, and it is claimed that the automatic proof procedure based on it ``provides some readability of the [synthetic] proofs'', which the algebraic approach does not. There is a wealth of notation and definitions with no intuitive explanation of what is being proposed, so only the most dedicated reader will find out what the advantage of this approach actually is. For the entire collection see [Zbl 0927.00010].