Representational change is integral to reasoning.

Reasoning is the derivation of new knowledge from old. The reasoner must represent both the old and new knowledge. This representation will change as reasoning proceeds. This change will not just be the addition of the new knowledge. We claim that the representation of the old knowledge will also often change as a side effect of the reasoning process. For instance, the old knowledge may contain errors, be insufficiently detailed or require new concepts to be introduced. Representational change triggered by reasoning is a common feature of human reasoning but it has been neglected both in Cognitive Science and Artificial Intelligence. We aim to put that right. We exemplify this claim by analysing Imre Lakatos's rational reconstruction of the evolution of mathematical methodology. We then describe the abduction, belief revision and conceptual change (ABC) theory repair system, which can automate such representational change. We further claim that the ABC system has a diverse range of applications to successfully repair faulty representations. This article is part of a discussion meeting issue 'Cognitive artificial intelligence'.

The interaction of representation and reasoning.

Automated reasoning is an enabling technology for many applications of informatics. These applications include verifying that a computer program meets its specification; enabling a robot to form a plan to achieve a task and answering questions by combining information from diverse sources, e.g. on the Internet, etc. How is automated reasoning possible? Firstly, knowledge of a domain must be stored in a computer, usually in the form of logical formulae. This knowledge might, for instance, have been entered manually, retrieved from the Internet or perceived in the environment via sensors, such as cameras. Secondly, rules of inference are applied to old knowledge to derive new knowledge. Automated reasoning techniques have been adapted from logic, a branch of mathematics that was originally designed to formalize the reasoning of humans, especially mathematicians. My special interest is in the way that representation and reasoning interact. Successful reasoning is dependent on appropriate representation of both knowledge and successful methods of reasoning. Failures of reasoning can suggest changes of representation. This process of representational change can also be automated. We will illustrate the automation of representational change by drawing on recent work in my research group.

What is a proof?

To those brought up in a logic-based tradition there seems to be a simple and clear definition of proof. But this is largely a twentieth century invention; many earlier proofs had a different nature. We will look particularly at the faulty proof of Euler's Theorem and Lakatos' rational reconstruction of the history of this proof. We will ask: how is it possible for the errors in a faulty proof to remain undetected for several years-even when counter-examples to it are known? How is it possible to have a proof about concepts that are only partially defined? And can we give a logic-based account of such phenomena? We introduce the concept of schematic proofs and argue that they offer a possible cognitive model for the human construction of proofs in mathematics. In particular, we show how they can account for persistent errors in proofs.