Proof Style?

John Harrison

University of Cambridge Computer Laboratory

New Museums Site

Pembroke Street

Cambridge CB2 3QG

England

[email protected]

http://www.cl.cam.ac.uk/users/jrh

January 1997

Abstract

We are concerned with how to communicate a mathematical proof to a computer theorem prover. This can be done in many ways, while allowing the machine to generate a completely formal proof object. The most obvious choice is the amount of guidance required from the user, or from the machine perspective, the degree of automation provided. But another important consideration, which we consider particularly significant, is the bias towards a `procedural' or `declarative' proof style. We will explore this choice in depth, and discuss the strengths and weaknesses of declarative and procedural styles for proofs in pure mathematics and for verification applications. We conclude with a brief summary of our own experiments in trying to combine both approaches.

?This is the text accompanying my invited talk at the European BRA Types annual meeting in Aussois. This talk was given on the 16th of December 1996, and the present text has been slightly modified in the light of some of the subsequent discussion.