TR.plausible.html

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