On Mathematical Proving and Algebra
We propose a formal description of a system suitable for the
representation of proving attempts towards the solution of
mathematical problems. The basic components include:
(1) the initial attempts for a solution;
(2) the variety of observations on the attempted solutions;
(3) alternative solutions or attempts emerging from the conclusions
drawn from observations;
(4) alternative proving strategies.
These components are repeatable - generating more refined attempted
solutions - until the problem is finally solved.
The starting-point of our theoretical work was provided by the paper
of J. Goguen "Sheaf Semantics for Concurrent Interactive Objects".
Initially we define as provers the objects which have sequences of
sentences as observable behaviour; we then construct systems of
provers and finally we define a Prover as a "Large" object.
Asterios Gatzounis
Last modified: Wed May 22 2024