Towards a Classification of Proofs

Manfred Kerber

In this talk different views on the concept of proof are presented. I advocate that the traditional view of Hilbert is only partly describing a multicoloured concept. Recent advances in the mechanisation of proof (in particular, the integration of computer algebra systems and mechanised reasoning systems) makes it necessary to deal with very long proofs. In agent-oriented proof search it is also necessary to communicate partial proofs efficiently. In order to do that effectively and efficiently it is necessary to write and communicate proofs on different levels. In the presentation I discuss important different dimensions of proofs, in particular

  • the formal system in which the proof is formulated (like natural deduction, tableau, resolution);
  • the rigour of the proof (in Polya's terminology to distinguish between demonstrative proofs and plausible proofs);
  • the problem formulation (is the theorem proved in the system it is originally stated or in a reformulated way);
  • the completeness of the proof (whether it is given in full detail or whether a lot of computation is required to construct it);
  • whether it is concise (the most concise form of a proof can be a triple consisting of the theorem, a theorem prover, and the number of steps performed by the prover to construct a proof);
  • the probabilistic level (primality tests, e.g., often demonstrate primality with high probability, but do not guarantee a property);
  • the information content (some faulty proofs can be easily patched, others do not contain any useful information).

    • Slides in both gzipped Postscript (118k), and PDF (235k)