Structured derivations (SD) is a logic-based format for presenting mathematical solutions and proofs created by Prof. Ralph-Johan Back and Joakim von Wright at Åbo Akademi University, Turku, Finland. The format was originally introduced as a way for presenting proofs in programming logic, but was later adapted to provide a practical approach to presenting proofs and derivations in mathematics education including exact formalisms. A structured derivation has a precise mathematical interpretation, and the syntax and the layout are precisely defined. The standardized syntax renders the format suitable for presenting and manipulating mathematics digitally.
Contents
SD is a further development of the calculational proof format introduced by Edsger W. Dijkstra and others in the early 1990s. In essence, three main extensions have been made. First, a mechanism for decomposing proofs through the use of subderivations has been added. The calculational approach is limited to writing proof fragments, and longer derivations are commonly decomposed into several separate subproofs. Using SD with subderivations, on the other hand, the presentation of a complete proof or solution is kept together, as subproofs can be presented exactly where they are needed. In addition, SD makes it possible to handle assumptions and observations in proofs. As such, the format can be seen as combining the benefits of the calculational style with the decomposition facilities of natural deduction.
Examples
The following three examples will be used to illustrate the most central features of structured derivations.
A simple equation
Solving a simple equation illustrates the basic structure of a structured derivation. The start of the solution is indicated by a bullet (
Each step in the solution consists of two terms, a relation and a justification that explains why the relationship between the two terms hold. The justifications are given equal amount of space as the mathematical terms in order to indicate the importance of explanations in mathematics.
Assumptions and observations
Specifications of mathematical problems commonly contain information that can be used in the solution. When writing a proof or a solution as a structured derivation, all known information is listed in the beginning as assumptions. These assumptions can be used to create new information that will be useful for solving the problem. This information can be added as observations that build on the assumptions. The following example uses two assumptions ((a)–(b)) and two observations ([1]–[2]). The introductory part of the solution (the task, assumptions and observations) is separated from the proof part by the
Sea water, where the mass-volume percentage of salt is 4.0%, is vaporized in a pool until its mass has decreased by 28%. What is the concentration of salt after the vaporization?
Subderivations
When solving a mathematical problem or constructing a proof, there is often a need to solve smaller problems in order to solve the entire problem. These subsolutions or subproofs are commonly written as fragments on the paper. SD introduces a mechanism for handling this type of subsolutions in a way that keeps these together with the remaining solution in one single chain. These subderivations are indented and the return to the original level is indicated with an ellipsis (
Teaching experience
Starting in 2001, SD has been empirically evaluated at different education levels with students aged 15–24. The most extensive study so far was a three-year-long quasi experiment conducted at a Finnish high school, where the test group was taught the compulsory mathematics courses using SD and the control group studied according to the traditional approach. The results indicate that the students in the test group performed better in all courses and the matriculation examination, even when potentially influencing factors have been taken into account. Other studies have indicated that students learn to justify their solutions during one single course and that students appreciate the new approach to writing mathematics.