TY - GEN
T1 - A proposal for automating diagrammatic reasoning in continuous domains
AU - Winterstein,Daniel
AU - Bundy,Alan
AU - Jamnik,Mateja
PY - 2000
Y1 - 2000
N2 - This paper presents one approach to the formalisation of diagrammaticproofs 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 amechanised construction of sequences of diagrams constituting a proof.This approach involves creating a diagrammatic theory. The method isjustified formally by (a) a diagrammatic axiomatisation, and (b) an appealto 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).
AB - This paper presents one approach to the formalisation of diagrammaticproofs 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 amechanised construction of sequences of diagrams constituting a proof.This approach involves creating a diagrammatic theory. The method isjustified formally by (a) a diagrammatic axiomatisation, and (b) an appealto 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).
U2 - 10.1007/3-540-44590-0_26
DO - 10.1007/3-540-44590-0_26
M3 - Conference contribution
SN - 978-3-540-67915-8
T3 - Lecture Notes in Computer Science
SP - 286
EP - 299
BT - Theory and Application of Diagrams
PB - Springer Berlin Heidelberg
ER -