Tools for the automated analysis of proofs

Research project P 14126 Tools for the automated analysis of proofs Matthias BAAZ 06.03.2000 There are many tools in Symbolic Computation supporting scientists and technicians, but only few deal with the automated analysis of given proofs or documented decisions. There will be a demand for such tools in the near future for the following reasons: * Mathematical proofs are the foundation of practical mathematical knowledge. Structures and theories are developed in accordance with the establishment of reasonable proofs. Long term progress in automated theorem proving for mathematics will be possible only if uptodate proofs become analyzable automatically and consequently proof styles - the results of these analyses - are incorporated into automated theorem provers. * The increase of mathematical knowledge will make it necessary for more and more mathematicians to work in a hybrid way in the near future, i.e. to establish proof plans who`s details are completed by the computer. The interaction between mathematician and computer however depends on the ability of the system to analyze and comprehend proof segments provided by the mathematician. * Furthermore, the analysis of proofs leads itself to new mathematical results, e.g. the extraction of numerical bounds and algorithms as well as the generalization of proofs, for example showing the independence of given proofs from certain assumptions. The automatization of this investigation will help the working mathematician to enrich his results by additional useful informations at low costs. This project is intended to develop and implement algorithms for the analysis of proofs based on proof theoretic methods, in particular on refinements of cut elimination and e -elimination. This research is connected to a further development of the theory of (computational aspects of) Skolem functions and the investigation of corresponding mathematical proofs as the van der Wærden and Schütte solution to Euler`s famous problem on the placement of thirteen points on a sphere with distance equal to the radius. Intended applications of the implemented algorithms to given formalized proofs will include * the extraction of Herbrand sequents from (segments of) possible non-constructive proofs. Bounds, realizing terms and algorithms depending on various parameters can be obtained from these tautologies. * the unwinding of implicitely defined concepts by explicit definitions using Maehara`s construction of interpolants for cut free proofs. * the construction of term minimal generalized proofs to establish independence of the proof from relevant parameters. * the calculation of generalized segments of proofs to use them as modules in other proofs. This will constitute a basis for the automatized development of proof styles as described above.

There are many tools in Symbolic Computation supporting scientists and technicians, but only few deal with the automated analysis of given proofs or documented decisions. There will be a demand for such tools in the near future for the following reasons: Mathematical proofs are the foundation of practical mathematical knowledge. Structures and theories are developed in accordance with the establishment of reasonable proofs. The increase of mathematical knowledge will make it necessary for more and more mathematicians to work in a hybrid way in the near future, i.e., to establish proof plans who`s details are completed by the computer. Furthermore, the analysis of proofs leads itself to new mathematical results, e.g. the extraction of numerical bounds and algorithms as well as the generalization of proofs, for example showing the independence of given proofs from certain assumptions. The automatization of this investigation will help the working mathematician to enrich his results by additional useful informations at low costs. In this project we have investigated and established logical methods for the analysis of proofs. The most important procedure is cut-elimination, which is able to transform highly indirect proofs into direct derivations allowing for the extraction of bounds, Herbrand disjunctions and interpolants. We created by the implementation of CERES an efficient tool for the automated analysis mentioned and applied it to various proofs from the literature (e.g. to a topological proof for the infinity of primes)