1. Notion of formal calculation system

1.1 Reasons for the development of formal calculus

Insofar as many calculations can be carried out using automated procedures, it is logical to consider having them carried out by a computer. The first programs to perform complex symbolic calculations were developed in the 60s by theoretical physicists in the fields of celestial mechanics, general relativity and, above all, atomic physics for the study of elementary particles.

The most frequently cited example is the algebraic calculation of the Moon's ephemeris, carried out by hand by French astronomer C. Delaunay. Delaunay from 1847 to 1867. A symbolic calculation program created in 1970 by A. Deprit, J. Henrard and A. Rom of the Boeing Company was able to reproduce and verify all Delaunay's calculations in...