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