Efficient computations in formal proofs

Henk Barendregt

Date: July 17th (Wednesday)
Time: ??.??
Abstract
Formal proofs in mathematics and computer science are being studied because these objects can be verified by a very simple computer program. An important open problem is whether these formal proofs can be generated with an effort not much greater than writing a mathematical paper in, say, (La)TeX. Modern systems for proof-development make the formalization of reasoning relatively easy. Formalizing computations such that the results can be used in formal proofs is not immediate. In this paper it is shown how to obtain formal proofs of statements like Prime(n) in the context of Peano arithmetic or x2-1=(x-1)(x+1) in the context of rings. It is hoped that the method will help bridge the gap between systems of computer algebra and systems of proof-development.

______________
__________________________________________

Previous page RISC SWP Linz Austria