A proposal for automating diagrammatic reasoning in continuous domains

Daniel Winterstein, Alan Bundy, Mateja Jamnik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper presents one approach to the formalisation of diagrammatic
proofs as an alternative to algebraic logic. An idea of ‘generic diagrams’ is developed whereby one diagram (or rather, one sequence of diagrams) can be used to prove many instances of a theorem. This allows the extension of Jamnik’s ideas in the Diamond system to continuous domains. The domain is restricted to non-recursive proofs in real analysis whose statement and proof have a strong geometric component.
The aim is to develop a system of diagrams and redraw rules to allow a
mechanised construction of sequences of diagrams constituting a proof.
This approach involves creating a diagrammatic theory. The method is
justified formally by (a) a diagrammatic axiomatisation, and (b) an appealt
o analysis, viewing the diagram as an object in R2. The idea is to then establish an isomorphism between diagrams acted on by redraw rules and instances of a theorem acted on by rewrite rules. We aim to implement these ideas in an interactive prover entitled Rap (the Real Analysis Prover).
Original languageEnglish
Title of host publicationTheory and Application of Diagrams
Subtitle of host publicationFirst International Conference, Diagrams 2000 Edinburgh, Scotland, UK, September 1–3, 2000 Proceedings
PublisherSpringer
Pages286-299
Number of pages14
ISBN (Electronic)978-3-540-44590-6
ISBN (Print)978-3-540-67915-8
DOIs
Publication statusPublished - 2000

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume1889
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'A proposal for automating diagrammatic reasoning in continuous domains'. Together they form a unique fingerprint.

Cite this