Fuzzy statememts 

 

The tools for automatic theorem proving in euclidean geometry are well established in the case of constructions, i.e. those theorems that state properties of configurations of points constructed one after another. 

 

A distinction of the methods of proof can be made considering statements and translations being accurate or non-accurate.
An accurate statement describes explicitly all the exceptional cases, a non-accurate statement leaves the obvious exceptional cases unremarked.
 

Non-accurate translations into systems of equations do not consider special cases in which the equivalence fails;
accurate translations consider systems of equations and inequations and fully preserve equivalence.
 

 

A proof in the non-accurate case requires in particular to identify explicitly the exceptional configurations, hence results at the end in an accurate statement. 

 

.... 

 

 

The degeneracy of a configuration is strictly dependent on the assertion; for example, three collinear points can be degenerate if we consider a triangle with the vertices in them, but in Maclane 8_3 theorem this is not a degenerate configuration; two coincident points are usually considered degenerate, but some theorems may just state that two points constructed differently always coincide, and in this case the coincidence is not a degeneracy.

Proving a theorem inaccurately stated means identifying a set of degenerate configurations such that outside them no exceptional configuration exists; in some sense, proving it implies providing an accurate statement and a proof of it.
Allowing inaccurate statements is typical in euclidean geometry, and should not be disallowed.