Structured derivations: a unified proof style for teaching mathematics |
| |
Authors: | Ralph-Johan Back |
| |
Affiliation: | (1) Department of Curriculum, Teaching and Learning, Ontario Institute for Studies in Education of the University of Toronto, Toronto, ON, M5S 1V6, Canada |
| |
Abstract: | Structured derivations were introduced by Back and von Wright 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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|