A Tough Nut for Mathematical Knowledge Management

摘要

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.