Bundy, Alan

Gurr, Corin

Jamnik, Mateja

Winterstein, Daniel

Engineering and Physical Sciences Research Council (EPSRC)

2004-12-21T10:33:26Z

2004-12-21T10:33:26Z

2005-07

Centre for Intelligent Systems and their Applications

This project looks at using diagrammatic reasoning to prove mathematical theorems. The work is motivated by a need for theorem provers whose reasoning is readily intelligible to human beings. It should also have practical applications in mathematics teaching. We focus on the continuous domain of analysis - a geometric subject, but one which is taught using a dry algebraic formalism which many students find hard. The geometric nature of the domain makes it suitable for a diagram-based approach. However it is a difficult domain, and there are several problems, including handling alternating quantifiers, sequences and generalisation. We developed representations and reasoning methods to solve these. Our diagram logic isn't complete, but does cover a reasonable range of theorems. It utilises computers to extend diagrammatic reasoning in new directions – including using animation. This work is tested for soundness, and evaluated empirically for ease of use. We demonstrate that computerised diagrammatic theorem proving is not only possible in the domain of real analysis, but that students perform better using it than with an equivalent algebraic computer system.

4339395 bytes

application/pdf

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

en

University of Edinburgh. College of Science and Engineering. School of Informatics.

Diagrammatic Reasoning

Theorem Proving

Continuous Domain

Using Diagrammatic Reasoning for Theorem Proving in a Continuous Domain

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy