Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:A Proposal for Automating Diagrammatic Reasoning in Continuous Domains
Authors: Daniel Winterstein ; Alan Bundy ; Mateja Jamnik
Date:Sep 2000
Publication Title:Theory and Application of Diagrams (LNCS)
Publisher:Springer Berlin
Volume No:1889 Page Nos:257-292
DOI:10.1007/3-540-44590-0_26 ISBN/ISSN:978-3-540-67915-8
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 appeal to 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).
2000 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
author = { Daniel Winterstein and Alan Bundy and Mateja Jamnik },
title = {A Proposal for Automating Diagrammatic Reasoning in Continuous Domains},
publisher = {Springer Berlin},
year = 2000,
month = {Sep},
volume = {1889},
pages = {257-292},
doi = {10.1007/3-540-44590-0_26},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh