A Proof and Some Representations

  • Manfred KerberEmail author
Part of the Cognitive Systems Monographs book series (COSMOS, volume 22)


Hilbert defined proofs as derivations from axioms via the modus ponens rule and variable instantiation (this definition has a certain parallel to the ‘recognise-act cycle’ in artificial intelligence). A pre-defined set of rules is applied to an initial state until a goal state is reached. Although this definition is very powerful and it can be argued that nothing else is needed, the nature of proof turns out to be much more diverse, for instance, changes in representation are frequently done. We will explore some aspects of this by McCarthy’s ‘mutilated checkerboard’ problem and discuss the tension between the complexity and the power of mechanisms for finding proofs.


Automate Theorem Prover Proof Rule White Field Black Tile Instantiation Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. Ayer AJ (1936) Language, truth and logic, 2nd edn. Victor Gollancz Ltd, LondonGoogle Scholar
  2. Bancerek G (1995) The mutilated chessboard problem—checked by MIZAR. In: Matuszewski R (ed) The QED Workshop II, Warsaw University, pp 37–38Google Scholar
  3. Bundy A, Jamnik M, Fugard A (2005) What is a proof? Philos Trans R Soc 363(1835):2377–2391CrossRefzbMATHMathSciNetGoogle Scholar
  4. Descartes R (1637) Discours de la méthode.
  5. Feynman RP (1985) Surely you’re joking Mr. Feynman, Vintage, LondonGoogle Scholar
  6. Hardy G (1940) A mathematician’s apology. Cambridge University Press, LondonGoogle Scholar
  7. Herbrand J (1930) Recherches sur la théorie de la démonstration. Sci Lett Varsovie, Classe III Sci Math Phys 33Google Scholar
  8. Jamnik M, Kerber M, Pollet M, Benzmüller C (2003) Automatic learning of proof methods in proof planning. Logic J IGPL 11(6):647–673Google Scholar
  9. Kerber M, Pollet M (2006) A tough nut for mathematical knowledge management. In: Kohlhase M (ed) Mathematical knowledge management—4th international conference, MKM 2005. Springer, LNAI 3863. Bremen, Germany, pp 81–95Google Scholar
  10. Lakatos I (1976) Proofs and refutations. Cambridge University Press, LondonCrossRefzbMATHGoogle Scholar
  11. Matuszewski R (ed) (1995) The QED workshop II.
  12. McCarthy J (1964) A tough nut for proof procedures. AI Project Memo 16. Stanford University, Stanford, California, USAGoogle Scholar
  13. McCarthy J (1995) The mutilated checkerboard in set theory. In: Matuszewski (ed) pp 25–26.
  14. McCune W (1997) Solution of the Robbins problems. J Autom Reason 19(3):263–276CrossRefzbMATHMathSciNetGoogle Scholar
  15. Robinson JA (1965) A machine oriented logic based on the resolution principle. JACM 12:23–41CrossRefzbMATHGoogle Scholar
  16. Sloman A (1996) What sort of architecture is required for a human-like agent? In: Rao RK (ed) Foundations of rational agency. Kluwer, The NetherlandsGoogle Scholar
  17. Zinn C (2004) Understanding informal mathematical discourse. PhD thesis, Friedrich-Alexander Universität Erlangen-NürnbergGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  1. 1.Computer ScienceUniversity of BirminghamBirminghamUK

Personalised recommendations