Circumcenter of a triangle

Simple set-theoretic approach

This approach reflects the kind of comprehension general to learners at the age of about 10 years. However, this approach still lacks a proper formalisation of geometry. This example is also used in the description of the ISAC system, where further details can be found.

We postpone considerations about axiom systems to the case study with the area method below.

Specification

Text: Given a triangle by the points A, B, C in a plane, construct the circumcenter O of the triangle.

Specification:

• given : <math>\mathit{point}\; A,\; \mathit{point}\; B,\; \mathit{point}\; C</math>
• precondition : <math>\neg \mathit{collinear}\; A\; B\; C</math>
• find : <math>\mathit{point}\; O\;</math>
• postcondition : <math>\overline{OA} = \overline{OB} \;\land\; \overline{OB} = \overline{OC} \;\land\; \overline{OC} = \overline{OA}</math>

Program in GCL

The program constructs the center O of the circumcircle of a triangle A B C. The program takes all four points as formal arguments, which have names as actual values determined in the preceeding specification phase; the program could look like as follows:

 1  Program circumcenter A B C O =
 2    let (P_1, P_2) = Take <math>\epsilon</math> (Q_1, Q_2). Q_1 <math>\in</math> {A,B,C} <math>\land</math>
 3     	       	      	   	    	  	Q_2 <math>\in</math> {A,B,C}   Q_1 <math>\not=</math> Q_2
 4	 m_1 = Subproblem (Triangles, [geom, euclid, plane, median],
 5	       		  	      [geom, euclid, plane, 2circ]) P_1 P_2 m_1
 6	(P_3, P_4) = Take <math>\epsilon</math> (Q_1, Q_2). Q_1 <math>\in</math> {A,B,C} - {P_1,P_2} </math>
 7     	       	      	   	    	  	Q_2 <math>\in</math> {A,B,C} Q_1 <math>\not=</math> Q_2
 8	 m_2 = Subproblem (Triangles, [geom, euclid, plane, median],
 9	       		  	      [geom, euclid, plane, 2circ]) P_3 P_4 m_2
10    in O = Take \epsion O. m_1 <math>\cap</math> m_2

The tactics propagating the construction are Take and Subproblem, and these tactics either mark some of the given points A, B, C and produce and output a new geometric object respectively. Description of the program along the line numbers:

• 2-3 Take marks 2 different points P_1 P_2 selected from the set {A,B,C}. <math>\epsilon</math> is Hilbert's operator of choice.
• 4-5 Subproblem creates the perpendicular bisector m_1 of the selected points; how m_1 is created is left to the Subproblem. Subproblems carry in deduction, see below
• 6-7 select another pair of points (P_3, P_4)
• 8-9 create a second perpendicular bisector m_2 from (P_3, P_4)
• 10 intersects m_1 and m_2 yielding the circumcenter O, which is output as final result.

Combining computation and deduction

See the description of the ISAC system.

Approach based on the area method

This section adopts all notions and all notations from strictly, except two letters due to restrictions in this wiki: <math>\Sigma</math> and <math>\Pi</math> designate signed area and Pythagoras difference respectively. Also, the small capitals for <math>PRATIO, TRATIO, INTER</math> etc are not available here.

Specification

The non-degenerate conditions are given in the precondition. For a discussion of the postcondition see Question 1 below.

• given : <math>\mathit{point}\; A,\; \mathit{point}\; B,\; \mathit{point}\; C</math>
• precondition : <math>A\not=B\land B\not=C\land C\not=A \land\Sigma_{ABC}\not=0</math>
• find : <math>\mathit{point}\; O\;</math>
• postcondition : <math>\overline{OA} = \overline{OB} \;\land\; \overline{OB} = \overline{OC} \;\land\; \overline{OC} = \overline{OA}</math>

Constructive Geometry Statement

A specification given in the format of the area method is called Constructive Geometry Statement (CGS). The CGS contains all construction steps. For the running example that looks like:

• construction steps:
  • step_1,_perpendicular_bisector_<math>m_1</math>: <math>(PRATIO\;M_1\;A\;A\;B\;1/2 ),\;(TRATIO\;N_1\;M_1\;A\;1)</math>
  • step_2,_perpendicular_bisector_<math>m_2</math>: <math>(PRATIO\;M_2\;B\;B\;C\;1/2 ),\;(TRATIO\;N_2\;M_2\;B\;1)</math>
  • step 3, intersection <math>m_1\cap m_2 = O</math>: <math>(INTER\;O\;N_1\;M_1\;N_2\;M_2)</math>
• conclusion: <math>\overline{OA} = \overline{OB}</math>

The conclusion must be one equation, so we cannot express the full beauty of what we have constructed here (COULD WE ?) What we would like to have is

• conclusion: <math>\overline{OA} = \overline{OB} \;\land\; \overline{OB} = \overline{OC} \;\land\; \overline{OC} = \overline{OA}</math>

Another variant on the example would have the conclusion, that <math>m_1\cap m_2 = m_2\cap m_3 = m_3\cap m_1</math>, i.e. that all pairs of perpendicular bisectors intersect in one and the same point. But this variant goes beyond the bare construction of the circumcenter.

Formulas corresponding to the construction steps

We take a separate line for each elementary construction step followed by another line with the respective non-degenerate conditions (ndg-condition):

• step 1, perpendicular bisector <math>m_1</math>:
  • <math>(PRATIO\;M_1\;A\;A\;B\;1/2)</math>:
    • <math> A M_1||A B\;\land\;\frac{\overline{A M_1}}{\overline{A B}}=1/2 </math>
    • ndg: <math> A\not=B </math>
  • <math>(TRATIO\;N_1\;M_1\;A\;1)</math>:
    • <math> M_1 N_1\perp A B\;\land\;\frac{4\Sigma_{M_1 A N_1}}{\Pi_{M_1 A M_1}}=1 </math>
    • ndg: <math> A\not=B </math>

• step 2, perpendicular bisector <math>m_2</math>:
  • <math>(PRATIO\;M_2\;B\;B\;C\;1/2 )</math>:
    • <math> B M_2||B C\;\land\;\frac{\overline{B M_2}}{\overline{B C}}=1/2 </math>
    • ndg: <math> B\not=C</math>
  • <math>(TRATIO\;N_2\;M_2\;B\;1)</math>:
    • <math> M_2 N_2\perp B C\;\land\;\frac{4\Sigma_{M_2 B N_2}}{\Pi_{M_2 B M_2}}=1 </math>
    • ndg: <math> B\not=C</math>

• step 3, intersection <math>m_1\cap m_2 = O</math>:
  • <math> (INTER\;O\;N_1\;M_1\;N_2\;M_2) </math>
    • <math> \Sigma_{N_1 M_1 O}=0\;\land\;\Sigma_{N_2 M_2 O}=0 </math>
    • ndg: <math> N_1\not=M_1\;\land\;N_2\not=M_2\;\land\;N_1 M_1\neg{||}N_2 M_2 </math>

QUESTIONS

QUESTION 1: conclusions

As mentioned above the standard format of the CGS's conclusion does not cover what one could wish for the construction of the circumcenter. All these equalities capture some aspects of a circumcenter, and the respective conjunction all(?) the aspects:

• <math>\overline{OA} = \overline{OB}</math>
• <math>\overline{OB} = \overline{OC}</math>
• <math>\overline{OC} = \overline{OA}</math>

And all pairs of perpendicular bisectors intersect in one and the same point:

• <math>m_1\cap m_2 = m_2\cap m_3</math>
• <math>m_1\cap m_2 = m_1\cap m_3</math>
• <math>m_1\cap m_3 = m_2\cap m_3</math>

OBSERVATION: All of the above equalities can be proven from the steps given above --- RIGHT ?

QUESTION: Is there a principal objection to generalise the format of the conclusion to a conjunction of equalities ? I.e. refute a proof with the first 'false' equality in the conjunction ?

If the answer would be 'yes', the response times reported for GCLC would suggest that there would be no technical obstacles due to efficiency.

QUESTION 2: equivalent steps

Tutoring, as seen by Lucas-Interpretation, concerns help for the learner at intermediate steps. Giving maximum freedom to the learner causes handling a combinatorial explosion in the tutoring system.

So a tutoring system needs some notion of 'equivalent steps' a learner can do at a certain stage during a construction (in algebra this is simply algebraic equivalence modulo some simplifier).

Let us look at a simple case in the running example:

• step 1, perpendicular bisector <math>m_1</math>: exactly as above.

• step_2',_perpendicular_bisector_<math>m_3</math>: <math>(PRATIO\;M_3\;C\;C\;A\;1/2 ),\;(TRATIO\;N_3\;M_3\;C\;1)</math>
  • <math>(PRATIO\;M_3\;C\;C\;A\;1/2 )</math>:
    • <math> C M_3||C A\;\land\;\frac{\overline{C M_3}}{\overline{C A}}=1/2 </math>
    • ndg: <math> C\not=A</math>
  • <math>(TRATIO\;N_3\;M_3\;C\;1)</math>:
    • <math> M_3 N_3\perp C A\;\land\;\frac{4\Sigma_{M_3 C N_3}}{\Pi_{M_3 C M_3}}=1 </math>
    • ndg: <math> C\not=A</math>

That means, we have two different second steps

• (a) step 1 (perp.bisector of A B) and step 2 (perp.bisector of B C)
• (b) step 1 (perp.bisector of A B) and step 2' (perp.bisector of C A)

QUESTION: How can the area method support a notion of equivalence of step 2 with step 2' in the context of the given problem ?

HYPOTHESES related to this question:

• We need to collect all the formulas related to all the steps done so far during a construction (independently from who has done the step, the learner by a trial or the system by a suggestion how to proceed)

• Such a context containing the formulas of both steps 1,2 can be compared with another context containing steps 1,2' by some normal form:
  • a rewrite order on the reduction lemmas seams feasible, involving lexical ordering on the names of points
  • The occurences of constructed points is somehow 'symmetrical in (a) and (b), which probably could be detected by the area method's elimination lemmas:
    • <math>M_1,N_1, M_2,N_2</math> in (a)
    • <math>M_1,N_1, M_3,N_3</math> in (b)

QUESTION 3: interpolation towards postcondition

This section is more hypothtetical and primarily shall serve the purpose to find out, who else uses the concept of 'interpolant', and where it could be useful for the purpose of tutoring.

Given two sets A and B of formulas, an interpolant for the pair (A, B) is a formula P with the following properties:

1. A implies P ,
2. P ∧ B is unsatisfiable, and
3. P refers only to the common variables of A and B.

Interpolants are computed from refutations of proofs; refutation is a non-terminating process in principle, which raises architectural issues for systems employing this technology. Interpolants serve different purposes so far:

• Model checking uses the fairly old concept for predicate refinement for more than a decade.

• Recent work varies and extends the technique and applies it to invariant generation in program synthesis.

The latter application of interpolants motivated the following hypothesis in personal communication:

HYPOTHESIS: Interpolants can provide a kind of 'measure for distance between a given context and a postcondition'. One advantage of such a measure would be to produce suggestions, which step better could approach the final goal.