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.
|Title of host publication||From Animals to Robots and Back: Reflections on Hard Problems in the Study of Cognition |
|Subtitle of host publication||A Collection in Honour of Aaron Sloman|
|Editors||Jeremy L Wyatt, Dean D Petters, David Hogg|
|Publication status||Published - 11 Jul 2014|
|Name||Cognitive Systems Monographs|