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.