From Animals to Robots and Back: Reflections on Hard Problems in the Study of Cognition pp 65-73 | Cite as

# A Proof and Some Representations

## Abstract

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.

## Keywords

Automate Theorem Prover Proof Rule White Field Black Tile Instantiation Rule## References

- Ayer AJ (1936) Language, truth and logic, 2nd edn. Victor Gollancz Ltd, LondonGoogle Scholar
- Bancerek G (1995) The mutilated chessboard problem—checked by MIZAR. In: Matuszewski R (ed) The QED Workshop II, Warsaw University, pp 37–38Google Scholar
- Bundy A, Jamnik M, Fugard A (2005) What is a proof? Philos Trans R Soc 363(1835):2377–2391CrossRefzbMATHMathSciNetGoogle Scholar
- Descartes R (1637) Discours de la méthode. http://www.gutenberg.org/ebooks/13846
- Feynman RP (1985) Surely you’re joking Mr. Feynman, Vintage, LondonGoogle Scholar
- Hardy G (1940) A mathematician’s apology. Cambridge University Press, LondonGoogle Scholar
- Herbrand J (1930) Recherches sur la théorie de la démonstration. Sci Lett Varsovie, Classe III Sci Math Phys 33Google Scholar
- 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
- 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
- Lakatos I (1976) Proofs and refutations. Cambridge University Press, LondonCrossRefzbMATHGoogle Scholar
- Matuszewski R (ed) (1995) The QED workshop II. http://www.mcs.anl.gov/qed/index.html
- McCarthy J (1964) A tough nut for proof procedures. AI Project Memo 16. Stanford University, Stanford, California, USAGoogle Scholar
- McCarthy J (1995) The mutilated checkerboard in set theory. In: Matuszewski (ed) pp 25–26. http://www.mcs.anl.gov/qed/index.html
- McCune W (1997) Solution of the Robbins problems. J Autom Reason 19(3):263–276CrossRefzbMATHMathSciNetGoogle Scholar
- Robinson JA (1965) A machine oriented logic based on the resolution principle. JACM 12:23–41CrossRefzbMATHGoogle Scholar
- 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
- Zinn C (2004) Understanding informal mathematical discourse. PhD thesis, Friedrich-Alexander Universität Erlangen-NürnbergGoogle Scholar