Bundy, Alan

Grov, Gudmund

Raggi, Daniel

other

2017-07-20T12:50:59Z

2017-07-20T12:50:59Z

2016-11-29

The role of representation in reasoning has been long and widely regarded as crucial. It has remained one of the fundamental considerations in the design of information-processing systems and, in particular, for computer systems that reason. However, the process of change and choice of representation has struggled to achieve a status as a task for the systems themselves. Instead, it has mostly remained a responsibility for the human designers and programmers. Many mathematical problems have the characteristic of being easy to solve only after a unique choice of representation has been made. In this thesis we examine two classes of problems in discrete mathematics which follow this pattern, in the light of automated and interactive mechanical theorem provers. We present a general notion of structural transformation, which accounts for the changes of representation seen in such problems, and link this notion to the existing Transfer mechanism in the interactive theorem prover Isabelle/HOL. We present our mechanisation in Isabelle/HOL of some specific transformations identified as key in the solutions of the aforementioned mathematical problems. Furthermore, we present some tools that we developed to extend the functionalities of the Transfer mechanism, designed with the specific purpose of searching efficiently the space of representations using our set of transformations. We describe some experiments that we carried out using these tools, and analyse these results in terms of how close the tools lead us to a solution, and how desirable these solutions are. The thorough qualitative analysis we present in this thesis reveals some promise as well as some challenges for the far-reaching problem of representation in reasoning, and the automation of the processes of change and choice of representation.

http://hdl.handle.net/1842/22936

en

The University of Edinburgh

Daniel Raggi, Alan Bundy, Gudmund Grov, and Alison Pease. Automating change of representation for proofs in discrete mathematics. In Intelligent Computer Mathematics, pages 227-242. Springer, 2015.

Attribution-NonCommercial-ShareAlike 4.0 International

http://creativecommons.org/licenses/by-nc-sa/4.0/

automated reasoning

representation

transformation

interactive theorem proving

Searching the space of representations: reasoning through transformations for mathematical problem solving

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy