Observe properties of dynamic constructions

Proving means logically relating the givens via intermediate facts to the consequence to be proved.  Being aware of the intermediate facts is thus an important step in this process. OK Geometry is a tool for automated observation of dynamic constructions. Observations can be considered as hypotheses and potential intermediate steps in a proof. It is up to the user to select the relevant hypotheses and organise them into a proof.

OK Geometry can observe dynamic constructions made by some fo the common dynamic geometry software (Cabri, Cabri Express, GeoGebra, Z.u.L, JGEX, Sketchometry, OK Geometry). It detects (but not proves) a variety of properties, ranging from collinearity of points to harmonic quadruplets. It is possible to reduce the observations from the elementary ones to the advanced.

Observing a dynamic construction is quite simple: just read the dynamic construction with the Task command and press the Observe command. A list of detected properties appears. A click on a property provides a visual representation of it. 

Here is a simple example: In a right triangle ABC let D be the foot of the altitude from the vertex C. Let E and F be the incentres of the triangles ADB and BDC respectively. 

OK Geometry produces a list of detected properties of the (dynamic) construction described above. The length of the list depends on the level of the analysis. Note that some of the listed properties are trivial (e.g. the points A, D, B are collinear), others are not. 

For example, one may not be aware that the points A, E, F, B lay on the same circle.

Here is another example. In a right triangle ABC let D be the midpont of BC and let E be the foot of the altitude at C in the triangle ACD. 
Prove that the triangle EBD is similar to the triangle BAD.

Proving the similarity of triangles EBD and BED is probably not a trivial task at a high school level. OK Geometry observes several properties of the above configuration. One of them is shown below: The circles through AEB and through AEC intersect on the hypothenuse AB. Considering this properties and the intersection point can set the path to the proof for the similarity of the triangles EBD and BED.