Create deductive proofs




The prover in OK Geometry provides, when successful, human-readable deductive proofs 

With OK Geometry you can create deductive proofs of geometric properties of dynamic constructions. The proving process employs a variant of the Geometric Deductive Database method developed by Chou, Gao and Zhang. While not every statement can be proved using this method, a successful outcome yields a human-readable, top-down deductive proof. Although the resulting proof may sometimes lack elegance, it can, with a little effort, be refined into a standard format suitable for educational purposes.

Creating proofs of geometric properties with the Observe proof module in OK Geometry is straightforward. The starting point is a dynamic construction, ideally one created using explicit construction steps, avoiding implicit or optimisation-based procedures. Once the Observe proofs module is activated, you specify the property to be proved and, optionally, adjust the proving parameters; the system then either generates the proof or states that the used method was unsuccessful. To facilitate understanding of the steps of the obtained proof, graphic illustrations and comments are provided in the module.

The proving capabilities of OK Geometry are illustrated by the examples below.

Example 1. A simple proof

Given a right-angled triangle ABC with a right angle at C, let I be the incentre of ABC and H be the orthocentre of triangle ABI.
Prove that ∠IAH = ∠HIB.

When creating the initial construction, one can use the predesigned dynamic shape of a right triangle and commands for the triangle centres, or restrict oneself to the commands typically used in school-level constructions. The Observe proof module provides a proof.





The individual steps of the proof are justified either by a defining property of the construction, by an evident property (for example, the transitivity of a relation), or by a known properties of a certain geometric patterns. In this case, two patterns are cited in the proof: 1. Pairwise congruent adjacent angles form congruent angles. 2. The arms of two right angles form two pairs of congruent angles (or supplementary angles).




 





Example 2. The prover adds a point to the construction


When a proof cannot be derived from the data of the construction alone, the prover attempts to add a point to the construction in an appropriate way. Sometimes the augmented construction allows the proof to be completed. In our case, OK Geometry added point D, the circumcentre of triangle BCI, to the initial construction and then generated a proof in 20 steps.
 
Given a right-angled triangle ABC with a right angle at C, let I be the incentre of ABC and H be the orthocentre of triangle ABI.
Prove that |IH| = |AB|. 



 

Example 3. Non-standard construction steps

In principle, each point in the construction used in the proof must be tangibly related to previously declared points. When specific points do not meet this criterion, one can declare their relevant properties in a comment or allow OK Geometry to identify their properties by observation. The prover accepts such declared and/or observed properties in the proof as facts. However, the user must, of course, justify them.

To create the configuration of the example, we started from collinear points A, B, and C and constructed the two tangent circles. Then we used the non-standard command to create a line tangent to the two circles and the touching points D and E. Note that it is not explicitly clear how D or E is related to A, B, and C.

To allow the creation of the proof, we declared that the line DE is perpendicular to segments AD and BE. In the obtained proof, the declared properties are used as facts, as well as the observed properties that |AD| = |AC| and |BE| = |BC|.

 

A circle centred at point A is externally tangent at point C to a circle centred at point B. A common external tangent to both circles touches the first circle at point D and the second circle at point E.

Show that angle ECD is a right angle.

Comments

  • The default proof format is top-down. It is also possible to display, instead of a proof, only the geometric patterns used in deductions within the proof; this can serve as hints for constructing one's own proof.
  • The user can specify the level of knowledge supported by the proof: basic level (without using proportions), secondary school level, or advanced level.
  • The Observe proof module can be invoked directly from observing a geometric construction. A property detected through observation can be proved by right-clicking the line with that property.
  • The proof module also allows listing all properties of a given construction that cannot be proved using the employed method.

Download figures (png)

Download constructions (p)