Structured derivations: a unified proof style for teaching mathematics.

*(English)*Zbl 1217.03043Summary: Structured derivations were introduced by R.-J. Back and J. von Wright [Refinement calculus. A systematic introduction. New York: Springer (1998; Zbl 0949.68094)] as an extension of the calculational proof style originally proposed by E. W. Dijkstra and his colleagues. Structured derivations added nested subderivations and inherited assumptions to this style. This paper introduces further extensions of the structured derivation format, and gives a precise syntax and semantics for the extended proof style. The extensions provide a unification of the three main proof styles used in mathematics today: Hilbert-style forward chaining proofs, Gentzen-style backward chaining proofs and algebraic derivations and calculations (in particular, Dijkstra’s calculational proof style). Each of these proof styles can now be directly presented as a structured derivation. Even more importantly, the three proof styles can be freely intermixed in a single structured derivation, allowing different proof styles to be used in different parts of the derivation, each time choosing the proof style that is most suitable for the (sub)problem at hand. We describe here (extended) structured derivations, feature by feature, and illustrate each feature with examples. We show how to model the three main proof styles as structured derivations. We give an exact syntax for structured derivations and define their semantics by showing how a structured derivation can be automatically translated into an equivalent Gentzen-style sequent calculus derivation. Structured derivations have been primarily developed for teaching mathematics at the secondary and tertiary education level. The syntax of structured derivations determines the general structure of the proof, but does not impose any restrictions on how the basic notions of the underlying mathematical domain are treated. Hence, the style can be used for any kind of proofs, calculations, derivations, and general problem solving found in mathematics education at these levels. The precise syntax makes it easy to provide computer support for structured derivations.

##### MSC:

03F03 | Proof theory in general (including proof-theoretic semantics) |

00A35 | Methodology of mathematics |

03B35 | Mechanization of proofs and logical operations |

97E40 | Language of mathematics (educational aspects) |

97E50 | Reasoning and proving in the mathematics classroom |

##### Keywords:

structured derivations; proof styles; Gentzen-style proofs; Hilbert-style proofs; Dijkstra’s calculational proofs; teaching mathematics; high-school mathematics; proof format; sequent calculus
PDF
BibTeX
XML
Cite

\textit{R.-J. Back}, Formal Asp. Comput. 22, No. 5, 629--661 (2010; Zbl 1217.03043)

Full Text:
DOI

**OpenURL**

##### References:

[1] | Back R-J (1980) Correctness preserving program refinements: proof theory and applications. In: Mathematical center tracts, vol 131. Mathematical Centre, Amsterdam · Zbl 0451.68018 |

[2] | Back R-J (1988) A calculus of refinements for program derivations. Acta Inform 25: 593–624 · Zbl 0658.68018 |

[3] | Back R-J, Grundy J, von Wright J (1998) Structured calculational proof. Formal Aspects Comput 9: 469–483 · Zbl 0905.68139 |

[4] | Back R-J, Mannila L, Peltomäki M, Sibelius P (2008) Structured derivations: a logic based approach to teaching mathematics. In: FORMED 2008: formal methods in computer science education, Budapest |

[5] | Back R-J, Mannila L, Wallin S (2009) Student justifications in high school mathematics. In: CERME 6 |

[6] | Back R-J, Sjöberg M, von Wright J (2002) Field tests of the structured derivations method. Technical Report 491, TUCS, Turku Centre for Computer Science, Turku, Finland |

[7] | Back R-J, von Wright J (1998) Refinement calculus: a systematic introduction. In: Graduate texts in computer science. Springer, Berlin |

[8] | Back R-J, von Wright J (1999) A method for teaching rigorous mathematical reasoning. In: Proceedings of international conference on technology of mathematics, University of Plymouth, UK |

[9] | Church A (1940) A formulation of the simple theory of types. J Symb Logic 5: 56–68 · Zbl 0023.28901 |

[10] | Detlefs D, Nelson G, Saxe JB (2005) Simplify: a theorem prover for program checking. J ACM 52(3): 365–473 · Zbl 1323.68462 |

[11] | Dijkstra EW, Scholten CS (1990) Predicate calculus and program semantics. Springer, Berlin · Zbl 0698.68011 |

[12] | Dijkstra EW (2002) The notational conventions I adopted, and why. Formal Aspects Comput 14: 99–107 · Zbl 1029.68004 |

[13] | Dutertre B, de Moura L (2006) The Yices SMT solver. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA. http://yices.csl.sri.com/tool-paper.pdf . Aug 2006 |

[14] | Gordon MJC, Melham TF (1993) Introduction to HOL. Cambridge University Press, New York |

[15] | Gries D (1991) Teaching calculation and discrimination: a more effective curriculum. Commun ACM 34: 45–54 |

[16] | Gries D (1996) Teaching and learning formal methods. In: Improving the curriculum through the teaching of calculation and discrimination. Academic Press, London, pp 181–196 |

[17] | Gries D, Schneider F (1993) A logical introduction to discrete mathematics. Springer, Berlin · Zbl 0861.03001 |

[18] | Gries D, Schneider F (1995) Teaching math more effectively through calculational proofs. Am Math Monthly 102(8): 691–697 · Zbl 0875.00012 |

[19] | Lamport L (1995) How to write a proof. Am Math Monthly 102(7): 600–608 · Zbl 0877.00005 |

[20] | Mannila L, Wallin S (2009) Promoting students justification skills using structured derivations. In: ICMI 19 studies |

[21] | Owre S, Shankar N, Rushby J (1992) PVS: a prototype verification system. In: CADE 11, Saratoga Springs, NY |

[22] | Paulson LC (1990) Isabelle: the next 700 theorem provers. In: Odifreddi P (eds) Logic and computer science. Academic Press, London, pp 361–386 |

[23] | Peltomäki M, Back R-J (2009) An empirical evaluation of structured derivations in high school mathematics. In: ICMI-19 studies, Taipei, Taiwan |

[24] | Trybulec A (1980) The Mizar logic information language. In: Studies in logic, grammar and rhetoric, Bialystok, vol 1 |

[25] | Trybulec A, Rudnicki P (1999) On equivalents of well-foundedness: an experiment in Mizar. J Autom Reason 23: 197–234 · Zbl 0944.68168 |

[26] | van de Snepscheut JLA (1993) What computing is all about. Springer, Berlin · Zbl 0817.68006 |

[27] | van Gasteren AJM (1990) On the shape of mathematical arguments. In: Lecture notes in computer science. Springer, Berlin |

[28] | Wenzel M (1999) Isar–a generic interpretative approach to readable formal proof documents. In: Bertot Y, Dowek G, Hirschowitz A, Paulin C, Thery L (eds) Theorem proving in higher order logics, 12th international conference, TPHOLs’99. Lecture notes in computer science, vol 1690. Springer, Berlin |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.