Explore constructions
Create proving tasks of varying difficulty from simple construction
Exploring constructions is an easy-to-apply process for systematically augmenting a given construction with one or more points. Points are added by applying operations from a specified set, in all reasonable ways, to previously defined points. The process also identifies interesting properties of the augmented constructions. The main purpose of exploring constructions is to find interesting properties of the resulting constructions, for example, particular types of properties or properties that are more or less difficult to prove.
Exploring constructions is closely linked to the deductive proving module. It identifies properties within the generated extended constructions and attempts to prove them using the GDD method. This method provides a rough estimate of the difficulty involved in proving individual properties; an inability to complete the proof using this method is considered indicative of a difficult proof.
The result of the Exploring constructions process is an archive of properties associated with the generated augmented constructions. For each property, a description and a rough estimate of the difficulty of proving it are provided. Browsing the archive is accompanied by visualisations of the constructions and properties. Selected archive items can be transferred to the current project, either as a dynamic construction file or as an active construction that can be explored using any module.
Example
Let us consider the following simple configuration:
k : semicircle on segment AB
C: AC ⊥ AB
D: |CD| = |CA| and D ∊ k (so CD is tangent to k)
k : semicircle on segment AB
C: AC ⊥ AB
D: |CD| = |CA| and D ∊ k (so CD is tangent to k)
The properties of the construction are immediately apparent. We are going to augment it with a point E (currently represented as a random point) that gives rise to an interesting property, whose proof might be either simple or more challenging.
In exploration, there are more than 50 operations available for adding a point. Taking into account the possible arguments (points) for these operations yields nearly 700 different ways to construct point E. The actual number is lower, however, as we exclude constructions that are infeasible or in which the new point coincides with one of the points of the initial configuration.
From the list of generated constructions and identified properties, we present just two:
Let E = k(C,A) ⋂ k(B,D).
Prove that △ACE ~ △BDE .
The module rates the task as moderately difficult.
Prove that △ACE ~ △BDE .
The module rates the task as moderately difficult.
Let E = incentre of △ADC.
Prove: Points A, B, D and E are cyclic.
Prove: Points A, B, D and E are cyclic.
The module rates the task as difficult.
The module regards proving the property as difficult if it cannot carry out the proof itself without adding another point to the construction. It is quite possible, however, that the reader’s perception of the difficulty will be entirely different.
We will now augment the initial construction with two points, E and F. In constructing them, we restrict ourselves to two possible operations: finding the incentre of a triangle formed by existing points, and projecting a point onto the line passing through two other points. Out of the 640 possible constructions for points E and F (some of which are infeasible or degenerate), we present two examples with specific properties.
Recall the initial construction:
k : semicircle on segment AB
C: AC ⊥ AB
D: |CD| = |CA| and D ∊ k (so CD is tangent to k)
k : semicircle on segment AB
C: AC ⊥ AB
D: |CD| = |CA| and D ∊ k (so CD is tangent to k)
We will now augment the initial construction with two points, E and F. In constructing them, we restrict ourselves to two possible operations: finding the incentre of a triangle formed by existing points, and projecting a point orthogonally onto line passing through two other points. Out of the 640 possible constructions for points E and F (some of which are infeasible or degenerate), we present three examples with specific properties.
Let E = incentre of ABD.
Let F = projection of A onto line DE.
Prove that line BD is parellel to line CF.
The task is, according to the module, easy.
Let F = projection of A onto line DE.
Prove that line BD is parellel to line CF.
The task is, according to the module, easy.
Let E = incentre of △ABD.
Let F = incentre of △ADC.
Prove that points B, E and F are collinear.
The task is, according to the module, difficult.
Let F = incentre of △ADC.
Prove that points B, E and F are collinear.
The task is, according to the module, difficult.
Let E = projection of C onto line BD.
Let F = projection of A onto line DE.
Prove that lines AB, CE and DF are concurrent.
The task is, according to the module, difficult.
Let F = projection of A onto line DE.
Prove that lines AB, CE and DF are concurrent.
The task is, according to the module, difficult.Some comments
A key aspect of exploration is defining how difficult it is to prove specific properties of augmented constructions. A proof is considered difficult if the GDD method employed cannot complete it without adding new points. The user can specify whether the proving mechanism should use only simple inferences (without ratios), inferences accessible to a high-school student, or more advanced inferences (for example, Ceva's theorem in a triangle).When adding points to the base construction, previously added points may or may not be taken into consideration.