Abstract
In this contribution we address two related questions. Firstly, we want to shed light on the question how to use a representation formalism to represent a given problem. Secondly, we want to find out how different formalizations are related and in particular how it is possible to check that one formalization entails another. The latter question is a tough nut for mathematical knowledge management systems, since it amounts to the question, how a system can recognize that a solution to a problem is already available, although possibly in disguise. As our starting point we take McCarthy’s 1964 mutilated checkerboard challenge problem for proof procedures and compare some of its different formalizations.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
McCarthy, J.: A tough nut for proof procedures. Stanford Artificial Intelligence Project Memo No. 16 (1964), Available from http://www-formal.stanford.edu/jmc/
McCarthy, J.: The mutilated checkerboard in set theory. [13], 25–26, Available from http://www.mcs.anl.gov/qed/index.html
Paulson, L.C.: A simple formalization and proof for the mutilated chess board. Logic Journal of the IGPL 9, 475–485 (2001); Also published as Technical Report Computer Laboratory, University of Cambridge, 394 (May 1996)
Huet, G.: The mutilated checkerboard (Coq library) (1996), http://coq.inria.fr/contribs/checker.html
Bancerek, G.: The mutilated chessboard problem – checked by Mizar. [13], 37–38, Available from http://www.mcs.anl.gov/qed/index.html
McCune, W.: Another crack in a tough nut. Association for Automated Reasoning Newsletter 31, 1–3 (1995)
Andrews, P.B., Bishop, M.: On sets, types, fixed points, and checkerboards. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol. 1071, pp. 1–15. Springer, Heidelberg (1996)
Rudnicki, P.: The mutilated checkerboard problem in the lightweight set theory of Mizar. Technical Report TR96-09, Department of Computing Science, University of Alberta (1996)
Feynman, R.P.: Surely you’re joking Mr. Feynman. Vintage, London, UK (1985)
Farmer, W.M., Guttman, J.D., Thayer, F.J.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567–581. Springer, Heidelberg (1992)
Farmer, W.M.: An infrastructure for intertheory reasoning. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 115–131. Springer, Heidelberg (2000)
Ayer, A.J.: Language, Truth and Logic, 2nd edn, 1951st edn. Victor Gollancz Ltd, London (1936)
Matuszewski, R. (ed.): The QED Workshop II (1995), Available from http://www.mcs.anl.gov/qed/index.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kerber, M., Pollet, M. (2006). A Tough Nut for Mathematical Knowledge Management. In: Kohlhase, M. (eds) Mathematical Knowledge Management. MKM 2005. Lecture Notes in Computer Science(), vol 3863. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11618027_6
Download citation
DOI: https://doi.org/10.1007/11618027_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31430-1
Online ISBN: 978-3-540-31431-8
eBook Packages: Computer ScienceComputer Science (R0)