Protocols
A proof protocol may consist, for example, in the following phases:
• Formalization
• Formalization through points
• Algebraic translation
• Test phase
• Algebraic completion
• Geometric completion
• Formal proof
TEST PHASE
• the hypothesis variety has a non degenerate component on which the theorem is true, or it is true on every non degenerate component...
• Theorems with examples
...when you draw a construction this corresponds to an example: the deductions made by the system correspond to finding a thesis that is valid on the component of the construction defined by the example...
• the definition of non-degeneracy is part of the protocol...
• not every protocol is suitable for every theorem
• the result of testing of a theorem depends from the protocol...
Models (Kreuzer-Robbiano, Computational Commutative Algebra II)
Kinds of truth (Bulmer-Fearnely_Sander-Stokes) “The Kinds of Truth of Geometric Theorems”, in Automated deduction in geometry (Zurich, 2000), Lecture Notes in Comput. Sci. 2061, 129–142, Springer, Berlin, 2001