\chapter{The Area Method}
\label{sec:areaMethod}

In this chapter we will present the results needed for the
compreenshion of the proofs kept in the database. All the results
are presented without demonstrations, to see such demonstrations the
reader should look
into~\cite{Chou93,Chou96,Narboux04,Zhang95,Quaresma06}. 


We will use capital letters to denote points in the plane. We denote
$\overline{AB}$ the length of the oriented segment from $A$ to
$B$. Thus $\overline{AB}=-\overline{BA}$.

We will denote $\Delta ABC$ the triangle formed by points $A$, $B$, and
$C$. We denote by $S_{ABC}$ the {\em signed area} of the oriented
triangle $\Delta ABC$~\cite{Zhang95}.

The {\em signed area} $S_{ABC}$ of triangle $ABC$ is the usual area
with a sign depending on the order of the vertices $A$, $B$, and $C$:
if $A - B - C$ rotates counterclockwisely, $S_{ABC}$ is positive,
otherwise it is negative~\cite{Chou96}.

\section{Basic Lemmas about Signed Areas and Ratio of Segments}
\label{sec:signedareas}


The following properties of the signed area are used as basic
lemmas~\cite{Chou96}.

For any points $A$, $B$, $C$, and $D$, we have:

\begin{lema} \label{lema:L1}\label{lemma1} %[L1/-/P2.1]
  $S_{ABC}=S_{CAB}=S_{BCA}=-S_{ACB}=-S_{BAC}=-S_{CBA}$.
\end{lema}

\begin{lema}\label{lemma2.2}\label{lemma2} %[L2/-/P2.1] 
  $S_{ABC}=0$ iff $A$, $B$, and $C$ are collinear.
\end{lema}


\begin{defs} \label{def1}
  We use the notation $AB\parallel PQ$ to denote the fact that $A$, $B$, $P$,
  and $Q$ satisfy one of the following conditions: (1) $A=B$ or $P=Q$;
  (2) $A$, $B$, $P$, and $Q$ are on the same line; or (3) line $AB$
  and line $PQ$ do not have a common point.  
\end{defs} 



\begin{lema}\label{lemma2.3}\label{lemma3} %[L3/B.3/P2.7] 
  $PQ \parallel AB$ iff $S_{PAB}=S_{QAB}$, i.e., iff $S_{PAQB}=0$.
\end{lema}


\begin{defs}[Parallelogram] \label{def2}
  A parallelogram is a quadrilateral $ABCD$ such that $AB\parallel CD$,
  $BC\parallel AD$, and no three vertices are on the same line. 
\end{defs}


\begin{defs}[Ratio of parallel lines] \label{def3}
  Let $ABCD$ be a parallelogram and $P$, $Q$ be two points on $CD$. We
  define the ratio of two parallel line segments as follows~\cite{Chou95}:

$$
\ratio{PQ}{AB}=\ratio{PQ}{DC}
$$

\begin{center}
   \includegraphics[scale=0.6]{defRatioParallel.eps}
\end{center}
\end{defs}


\begin{lema}\label{lema:L4}\label{lemma4} %[L4/-/P2.1] 
  $S_{ABC}=S_{ABD}+S_{ADC}+S_{DBC}$.
  
  \begin{center}
    \includegraphics[scale=0.6]{prop2.2.3.eps}
  \end{center}
  
  $S_{ABC}=S_{ABD}+S_{ADC}+S_{DBC} \Leftrightarrow  a+c=(a+b)+(c+d)+(-b-d) \Leftrightarrow a+c=a+c$
\end{lema}  
  

\begin{lema} \label{lemma5} %[L5/B.1/P2.3] 
  If points $C$ and $D$ are on line $AB$, $A\neq B$ and $P$ is any point
  not on line $AB$ (Figure~\ref{fig:prop2.3}) then:
  
  $$
  \frac{S_{PCD}}{S_{PAB}} = \ratio{CD}{AB}.
  $$
  
  
  \begin{figure}[hbtp]
    \centering
    \includegraphics[scale=0.6]{prop2.3.eps}
    \caption{Areas, Ratios relationship}
    \label{fig:prop2.3}
  \end{figure}
  
\end{lema}


\begin{defs} \label{def4}
  $S_{ABCD}$ is defined as $S_{ABCD}=S_{ABC}+S_{ACD}$~\cite{Chou96,Narboux04}.  
\end{defs}


More generally we can define the signed area of an oriented $n$-polygon
$A_1A_2\ldots A_n$, $(n\geq3)$ to be~\cite{Zhang95}

$$
S_{A_1A_2\ldots A_n} = \sum_{i=3}^n S_{A_1A_{i-1}A_i}.
$$

by Lemmas \ref{lema:L1} and \ref{lema:L4}, we have.
  

\begin{lema} \label{lemma6} %[Q1/-/-] 
  $S_{ABCD}=S_{ABC}+S_{ACD}=S_{ABD}+S_{BCD}$.
\end{lema}

\begin{center}
  \includegraphics[scale=0.6]{prop2.2def.eps}
\end{center}

\begin{lema}\label{lemma7}  %[Q2/-/-]
  $S_{ABCD}=S_{BCDA}=S_{CDAB}=S_{DABC}=-S_{ADCB}=-S_{DCBA}=-S_{CBAD}=-S_{BADC}$. 
\end{lema}

Given the fact that we are speaking about {\em oriented areas}, we
have clock-wise, positive sign, and anticlock-wise, negative sign.


\begin{lema}[\eliminationlemma] \label{lemma2.8}\label{lemma8} % EL1\ - L6/B.2/P2.4
    (The Co-side Theorem) Let M be the intersection of two
    non-parallel lines $AB$ and $PQ$ and $Q\neq M$
    (Figure~\ref{fig:prop2.4}). Then:

  $$
  \ratio{PM}{QM} = \frac{S_{PAB}}{S_{QAB}};\quad \ratio{PM}{PQ} =
  \frac{S_{PAB}}{S_{PAQB}};\quad\ratio{QM}{PQ} =
  \frac{S_{QAB}}{S_{PAQB}}. 
  $$
  
  \begin{figure}[hbtp]
    \centering
    \includegraphics[scale=0.6]{prop2.4.eps}
    \caption{Co-side Theorem}
    \label{fig:prop2.4}
  \end{figure}
  
  Since $P_{PAB}$ and $S_{QAB}$ cannot both be zero, we always assume
  that the nonzero one is the denominator. Also note that
  $\overline{PQ}\neq0$ since $AB\not\parallel PQ$.
  
\end{lema}


\begin{lema}\label{lemma2.9}\label{lemma9} %[L7/B.4/P2.5] 
  Let $R$ be a point on line $PQ$. Then for any two points $A$ and $B$
  (Figure~\ref{fig:prop2.5})~\cite{Chou96,Zhang95}:

  $$
  S_{RAB}=\ratio{PR}{PQ}S_{QAB}+\ratio{RQ}{PQ}S_{PAB}
  $$
  
  
  \begin{figure}[hbtp]
    \centering
    \includegraphics[scale=0.5]{prop2.5.eps}
    \caption{\ }
    \label{fig:prop2.5}
  \end{figure}
\end{lema}  


For four collinear points $P$, $Q$, $A$, and $B$, such that $A\not=
B$, $\ratio{PQ}{AB}$, {\em the ratio of the directed segments}, is an
element in $\mathds R$, that satisfies the following
lemmas~\cite{Chou95,Chou96,Zhang95}.

\begin{lema}\label{lemma10} %[L8/-/P2.1] 

  $\ratio{PQ}{AB}= -\ratio{QP}{AB} = \ratio{QP}{BA} = -\ratio{PQ}{BA}$.
\end{lema}


\begin{lema}\label{lemma11} %[L8/-/P2.1] 
  $\ratio{PQ}{AB}=0$ iff $P=Q$.
\end{lema}

\begin{lema}\label{lemma12} %[L8/-/P2.1] 
  $\ratio{PQ}{AB}\times\ratio{AB}{PQ}=1$.
\end{lema}

\begin{lema} \label{lemma13} %[L8/-/P2.1]
  $\ratio{AP}{AB}+\ratio{PB}{AB}=1$.
\end{lema}

\begin{lema}\label{lemma14} %[L8/-/P2.1] 
  for each $r\in{\mathds R}$ there exists a unique point $P$ which is
  collinear with $A$ and $B$ and satisfies $\ratio{AP}{AB}=r$.
\end{lema}

  
  
Let $r=\ratio{PQ}{AB}$. We sometimes also write $\overline{PQ} =
r\overline{AB}$. A point $P$ on line $AB$ is determined uniquely by
$\ratio{AP}{AB}$ or $\ratio{PB}{AB}$. We thus call

$$
x_P = \ratio{AP}{AB},\qquad y_P=\ratio{PB}{AB}
$$
the {\em position ratio} or {\em position coordinates} of the point
$P$ with respect to $AB$. It is clear that $x_p+y_p=1$.


In our machine proofs, {\em auxiliary parallelograms} are often added
automatically and the following two propositions are used frequently.


\begin{lema}\label{lemma15} %[-/B.5/-]
  Let $ABCD$ be a parallelogram and $P$ be any point
  (fig.~\ref{fig:propB5}). Then~\cite{Chou95,Zhang95}
  
  $$
  S_{ABC}=S_{PAB}+S_{PCD} \qquad\mathrm{and}\qquad
  S_{PAB}=S_{PDAC}=S_{PDBC}~\cite{Zhang95}.
  $$
  
  $$
  S_{PAB}=S_{PCD}-S_{ACD}=S_{PDAC}~\cite{Chou95}.
  $$


  \begin{figure}[hbtp]
    \centering
    \includegraphics[scale=0.6]{propB5.eps}
    \caption{\ }
    \label{fig:propB5}
  \end{figure}
\end{lema}
  

\begin{lema}\label{lemma2.12}\label{lemma16} %[-/-/P2.8] 
  Let $ABCD$ be a parallelogram, $P$ and $Q$ be two points
  (Figure~\ref{fig:prop2.8}). Then~\cite{Zhang95}

$$
S_{APQ}+S_{CPQ}=S_{BPQ}+S_{DPQ}\quad\mathrm{or}\quad S_{PAQB}=S_{PDQC}.
$$
\end{lema}

Notice that $\Delta APQ$ and $\Delta BPQ$ are clockwise, and $\Delta CPQ$ and $\Delta DPQ$ are
anti-clockwise.

\begin{figure}[hbtp]
  \centering
   \includegraphics[scale=0.6]{prop2.8v1.eps}\qquad
    \includegraphics[scale=0.6]{prop2.8.eps}
  \caption{\ }
  \label{fig:prop2.8}
\end{figure}


\section{Basic Lemmas about Pythagoras Differences}
\label{sec:pitadifs}

\begin{defs}[Pythagoras difference] \label{def5}
  For three points $A$, $B$, and $C$, the {\em Pythagoras difference}
  $P_{ABC}$ is defined to be:
  
$$
P_{ABC}=\overline{AB}^2+\overline{CB}^2-\overline{AC}^2.
$$


\begin{center}
  \includegraphics[scale=0.6]{pitdifs.eps}
\end{center}
\end{defs}



\begin{lema} \label{lemma17}%[-/-/pre P2.12]
  $P_{AAB}=0$.
\end{lema}


\begin{lema}\label{lemma18} %[-/-/pre P2.12] 
  $P_{ABC}=P_{CBA}$.
\end{lema}


\begin{lema} \label{lemma19} %[-/-/pre P2.12]
  $P_{ABA}=2\overline{AB}^2$.
\end{lema}



\begin{lema}\label{lemma20} %[-/-/pre P2.12]
  If $A$, $B$, and $C$ are collinear them, $P_{ABC} = 2\overline{BA} \times
  \overline{BC}$. 
\end{lema}


\begin{defs} \label{def6}
  For a quadrilateral $ABCD$, we have

$$
P_{ABCD} = P_{ABD}-P_{CBD} = \overline{AB}^2 + \overline{CD}^2 -
\overline{BC}^2 - \overline{DA}^2.
$$
\end{defs}

\begin{lema}\label{lemma21} %[-/-/pre P2.12] 
  We have $P_{ABCD} = -P_{ADCB} = P_{BADC} = -P_{BCDA} =
  P_{CDAB} = -P_{CBAD} = P_{DCBA} = -P_{DABC}$.
\end{lema}


\begin{defs} \label{def7} %[-/-/def 2.11]
  For four points $A$, $B$, $C$, and $D$, the notation $AB\perp CD$ implies
  that one of the following conditions is true: $A=B$, or $C=D$, or
  the line $AB$ is perpendicular to line $CD$.
\end{defs}

\begin{lema}[Pythagorean Theorem] \label{lemma2.17}\label{lemma22}% [-/-/P2.12] 
  $AB\perp BC$ iff $P_{ABC}=0$.
\end{lema}


\begin{lema}\label{lemma2.18} \label{lemma23}%[-/-/P2.13] 
  $AB\perp CD$ iff $P_{ACD} = P_{BCD}$ or $P_{ACBD} = 0$ (figure~\ref{fig:p2.13}).

  \begin{figure}[hbtp]
    \centering
    \includegraphics[scale=0.6]{prop2.13.eps}
    \caption{\ }
    \label{fig:p2.13}
  \end{figure}

\end{lema}


The above generalised Pythagorean proposition is one of the most
useful tools in our mechanical theorem proving method.

\begin{lema} \label{lemma2.19}\label{lemma24} %[-/-/P2.14]
  Let $D$ be the foot of the perpendicular drawn from point $P$ to a
  line $AB$ (figure~\ref{fig:p2.14}). Then:

  $$
  \frac{\overline{AD}}{\overline{DB}} = \frac{P_{PAB}}{P_{PBA}}, \quad
  \frac{\overline{AD}}{\overline{AB}} = \frac{P_{PAB}}{2\overline{AB}^2}, \quad
  \frac{\overline{DB}}{\overline{AB}} = \frac{P_{PBA}}{2\overline{AB}^2}.
  $$

  \begin{figure}[hbtp]
    \centering
    \includegraphics[scale=0.6]{prop2.14.eps}
    \caption{\ }
    \label{fig:p2.14}
  \end{figure}
\end{lema}

\begin{lema} \label{lemma2.20}\label{lemma25} %[-/-/P2.15]
  Let $AB$ and $PQ$ be two non-perpendicular lines, and $Y$ be the
  intersection of line $PQ$ and the line passing through $A$ and
  perpendicular to $AB$ (figure~\ref{fig:p2.15}). Then:

  $$
  \frac{\overline{PY}}{\overline{QY}} = \frac{P_{PAB}}{P_{QAB}}, \quad
  \frac{\overline{PY}}{\overline{PQ}} = \frac{P_{PAB}}{P_{PAQB}}, \quad
  \frac{\overline{QY}}{\overline{PQ}} = \frac{P_{QAB}}{P_{PAQB}}.
  $$ 


  \begin{figure}[hbtp]
    \centering
    \includegraphics[scale=0.6]{prop2.15.eps}
    \caption{\ }
    \label{fig:p2.15}
  \end{figure}
\end{lema}

\begin{lema} \label{lemma2.21}\label{lemma26} %[-/-/P2.16]
  Let $R$ be a point on line $PQ$ with position ratios
  $r_1=\ratio{PR}{PQ}$, $r_2=\ratio{RQ}{PQ}$ with respect to $PQ$. Then
  for points $A$, $B$, we have (figure~\ref{fig:p2.16}):

  \begin{eqnarray*}
    P_{RAB} & = & r_1P_{QAB} + r_2P_{PAB} \\
    P_{ARB} & = & r_1P_{AQB} + r_2P_{APB} - r_1r_2P_{PQP}\ .
  \end{eqnarray*}
  \begin{figure}[hbtp]
    \centering
    \includegraphics[scale=0.6]{prop2.16.eps}
    \caption{\ }
    \label{fig:p2.16}
  \end{figure}
\end{lema}

\begin{lema}\label{lemma2.22}\label{lemma27} %[-/-/P2.17] 
  Let $ABCD$ be a parallelogram. Then for any points $P$ and $Q$, we
  have (figure~\ref{fig:p2.17}):

  \begin{eqnarray*}
    P_{APQ} + P_{CPQ} & = & P_{BPQ} + P_{DPQ}\quad\mathrm{or}\quad P_{APBQ}=P_{DPCQ}\\
    P_{PAQ} + P_{PCQ} & = & P_{PBQ} + P_{PDQ} + 2P_{BAD}\ .
  \end{eqnarray*}
  \begin{figure}[hbtp]
    \centering
    \includegraphics[scale=0.6]{prop2.17.eps}
    \caption{\ }
    \label{fig:p2.17}
  \end{figure}
\end{lema}




%%%%%%%%%%%%%%%%% falta acrescentar texto sobre o teorema da Linha de
%%%%%%%%%%%%%%%%% Gauss 



\section{The Constructive Geometry Statements}
\label{sec:consGeo}


\subsection{Constructive Geometry Statements}
\label{subsec:consGeo}

Points are the basic geometry objects, from which we can introduce two
other {\em geometric objects}: lines and circles.

A {\em straight line} can be given in one of the following four
forms. 

\begin{description}
\item[(LINE U V)] is the line passing through two points $U$ and $V$.
\item[(PLINE W U V)] is the line passing  through point $W$ and
  parallel to (LINE U V).
\item[(TLINE W U V)] is the line passing  through point $W$ and
  perpendicular to (LINE U V).
\item[(BLINE U V)] is the perpendicular bisector of $UV$.
\end{description}

To make sure that the four kinds of lines are well defined, we need to
assume that $U\neq V$ which is called the {\em non-degenerated condition}
(ndg) of the corresponding line.

\begin{description}
\item[(CIR O U)] denotes a {\em circle} with point $O$ as its center
  and passing through point $U$.
\end{description}


\paragraph{Constructions:}
\label{par:construction}
a {\em construction} is one of the following ways of introducing new
points. For each construction, we also give its ndg condition and the
degrees of freedom for the constructed point.


\begin{description}
\item[C1 -- (POINT\mbox{[S]} Y1, \ldots, Yn).] Take arbitrary points $Y_1$, \ldots,
  $Y_n$ in the plane. Each $Y_i$ has two degrees of freedom.
\item[C2 -- (ON Y ln).] Take a point $Y$ on a line $ln$. The ndg
  condition of C2 is the ndg condition of the line $ln$. A point $Y$
  has one degree of freedom.
\item[C3 -- (ON Y (Cir O P)).]  Take a point $Y$ on a circle (CIR O
  P). The ndg condition is $O\neq P$. Point $Y$ has one degree of freedom.
\item[C4 -- (INTER Y ln1 ln2).] Point $Y$ is the intersection of line
  $ln_1$ and line $ln_2$. Point $Y$ is a fixed point. The ndg
  condition is $ln_1\not\parallel ln_2$. More precisely, we have:
  \begin{enumerate}
  \item If $ln_1$ is (LINE U V) or (PLINE W U V) and $ln_2$ is (LINE P
    Q) or (PLINE R P Q), the ndg condition is $UV\not\parallel PQ$.
  \item If $ln_1$ is (LINE U V) or (PLINE W U V) and $ln_2$ is (BLINE P
    Q) or (TLINE R P Q), then the ndg condition is $UV\notperp PQ$.
  \item If $ln_1$ is (BLINE U V) or (TLINE W U V) and $ln_2$ is (BLINE
    P Q) or (TLINE R P Q), then the ndg condition is $UV\not\parallel PQ$.
  \end{enumerate}
\item[C5 -- (INTER Y ln (CIR O P)).] Point $Y$ is the intersection of
  line $ln$ and circle (CIR O P) other than point $P$. Line $ln$ could
  be (LINE P U), (PLINE P U V), or (TLINE P U V). The ndg conditions
  are $O\neq P$, $Y\neq P$, and line $ln$ is not degenerate. Point $Y$ is a
  fixed point.
\item[C6 -- (INTER Y (CIR O1 P) (CIR O2 P)).] Point $Y$ is the
  intersection of the circle (CIR O1 P) and the circle (CIR O2 P)
  other them point $P$. The ndg condition is that $O_1$, $O_2$, and
  $P$ are not collinear. Point $Y$ is a fixed point.
\item[C7 -- (PRATIO Y W U V r).] Take a point $Y$ on the line (PLINE W
  U V) such that $\overline{WY}=r\overline{UV}$, where $r$ can be a
  rational number, a rational expression in geometric quantities, or a
  variable.

  If $r$ is a fixed quantity the $Y$ is a fixed point; if $r$ is a
  variable the $Y$ has one degree of freedom. The ndg condition is $U\neq
  V$. If $r$ is a rational expression in geometric quantities the we
  will further assume that the denominator of $r$ could not be zero.
\item[C8 -- (TRATIO Y U V r).] Take a point $Y$ on line (TLINE U U V)
  such that $r = \frac{4S_{UVY}}{P_{UVU}}( =
  \frac{\overline{UY}}{\overline{UV}})$, where $r$ can be a rational
  number, a rational expression in geometric quantities, or a
  variable.

  If $r$ is a fixed quantity then $Y$ is a fixed point; if $r$ is a
  variable $Y$ has one degree of freedom. The ndg condition is the
  same as that of C7.
\end{description}

Since there are four kinds of lines, constructions C2, C4, C5 have 4,
10, 3 possible forms respectively. Thus, totally we have 22 different
forms of constructions.

\begin{defs}[Class of Constructive Geometry Statements] \label{def8}
  The class of {\em Constructive Geometry Statements}, $\mathbf{C}$,
  is the class of statements defined as follows. A statement in class
  $\mathbf{C}$ is a list $S=(C_1,C_2,\ldots,C_n,G)$ where $C_i$ for $1\leq
  i\leq n$ are constructions such that each $C_i$ introduces a new point
  from the points introduced before; and $G=(E_1,E_2)$ where $E_1$ and
  $E_2$ are polynomials in geometric quantities of the points
  introduced by the $C_i$ and $E_1=E_2$ is the conclusion of the
  statement. 
\end{defs}

Let $S=(C_1,C_2,\ldots,C_n,(E_1,E_2))$ be a statement in  $\mathbf{C}$. The
ndg condition of $S$ is the set of ndg conditions of the $C_i$s plus
the condition that the denominators of the length ratios in $E_1$
and $E_2$ are not equal to zero.

The 22 constructions are not independent to each other. We now
introduce a minimal set of constructions which are equivalent to all
the 22 constructions but much few in number.

A {\em minimal set of constructions} consist of C1, C7, C8, and the
following two constructions.


\begin{description}
\item[C41 -- (INTER Y (LINE U V) (LINE P Q))].
\item[C42 -- (FOOT Y P U V)] or equivalently (INTER Y (LINE U V)
  (TLINE P U V)). The ndg condition is $U\neq V$.
\end{description}

We first show how to represent the four kinds of lines by one kind:
(LINE U V). 

For $ln=$(PLINE W U V), we first introduce a new point $N$ by (PRATIO
N W U V 1). Then $ln=$(LINE W N).

For $ln=$(TLINE W U V), we have two cases: if $W$, $U$, $V$ are
collinear, $ln=$(LINE N W) where $N$ is introduced by (TRATIO N W U
1); otherwise $ln=$(LINE N W) where $N$ is given by (FOOT N W U V).

(BLINE U V) can be written as (LINE N M) where $N$ and $M$ are
introduced as follows (MIDPOINT M U V) (i.e. (PRATIO M U U V 1/2)),
and (TRATIO N M U 1).

Since now there is only one kind of line, to represent all the 22
constructions by the constructions in the minimal set we only need to
consider the following cases.

\begin{itemize}
\item (ON Y (LINE U V)) is equivalent to (PRATIO Y U U V r) where $r$
  is an {\em indeterminate}.
\item (INTER Y (LINE U V) (CIR O U)) is equivalent to two
  constructions: (FOOT N O U V), (PRATIO Y N N U -1).
\item C6 can be reduced to (FOOT N P O1 O2) and (PRATIO Y N N P -1).
\item For C3, i.e., to take an arbitrary point $Y$ on a circle (CIR O
  P), we first take an arbitrary point $Q$. Then $Y$ is introduced by
  (INTER Y (LINE P Q) (CIR O P)).
\end{itemize}



\section{The Algorithm}
\label{sec:algorithm}

The key step of the method is to {\em eliminate points from geometry
  quantities}. The point are introduced naturally and are eliminated
from the conclusion in the reverse order.


\subsection{The Elimination Procedures}
\label{sec:elimproc}

Considering only the minimal set of constructions: C1, C7, C8, C41,
and C42 we need only to eliminate points introduced by four
constructions from three kinds of geometry quantities.


\begin{lema}\label{lemma4.0} \label{lemma28} %[-/-/P2.17] 
Let $G(Y)$ be one of the following geometry quantities: $S_{ABY}$,
$S_{ABCY}$, $P_{ABY}$, or $P_{ABCY}$ for distinct points $A$, $B$,
$C$, and $Y$. For three collinear points $Y$, $U$, and $V$, by
lemmas~\ref{lemma2.9} and~\ref{lemma2.21} we have:

\begin{equation}
  \label{eq:I}
  G(Y) = \frac{\overline{UY}}{\overline{UV}}G(V) +
  \frac{\overline{YV}}{\overline{UV}}G(U).
\end{equation}
\end{lema}

We call $G(Y)$ a {\em linear geometry quantity} for variable
$Y$. Elimination procedures for all linear geometry quantities are
similar for constructions C7, C41, and C42.






\begin{lema}[\eliminationlemma] \label{lemma4.1}\label{lemma29} % EL2
  Let $G(Y)$ be a linear geometry quantity and point $Y$ be introduced
  by construction (PRATIO Y W U V r). Then we have:

  $$
  G(Y)=G(W)+r(G(V)-G(U)).
  $$
\end{lema}



\begin{lema}[\eliminationlemma] \label{lemma4.2}\label{lemma30} % EL3
  Let $G(Y)$ be a linear geometry quantity and point $Y$ be introduced
  by construction (INTER Y (LINE U V) (LINE P Q). Then we have: 

  $$
  G(Y)=\frac{S_{UPQ}G(V)-S_{VPQ}G(U)}{S_{UPVQ}}.
  $$
   
\end{lema} 



\begin{lema}[\eliminationlemma]  \label{lemma4.3}\label{lemma31}  % EL4
  Let $G(Y)$ be a linear geometry quantity ($\neq P_{AYB}$) and point $Y$
  be introduced by construction (FOOT Y P U V). Then we have:

  $$
  G(Y)=\frac{P_{PUV}G(V)+P_{PVU}G(U)}{2\overline{UV}^2}.
  $$
\end{lema}


\begin{lema}[\eliminationlemma]  \label{lemma4.4}\label{lemma32}   % EL5
  Let $G(Y) = P_{AYB}$ and point $Y$ be introduced by construction
  (FOOT Y P U V) or (INTER Y (LINE U V) (LINE P Q)). Then we have:

\begin{equation}
  \label{eq:II}
  G(Y)  =  \frac{\overline{UY}}{\overline{UV}}G(V) +
  \frac{\overline{YV}}{\overline{UV}}G(U) -
  \frac{\overline{UY}}{\overline{UV}} \cdot
  \frac{\overline{YV}}{\overline{UV}}P_{UVU}. 
\end{equation}
\end{lema}


\begin{lema}[\eliminationlemma] \label{lemma4.5}\label{lemma33}  % EL6 \quad -/-/L4.4
  Let $Y$ be introduced by (PRATIO Y W U V r). Then we have:

  $$
  P_{AYB} = P_{AWB}+r(P_{AVB}-P_{AUB}+P_{WUV}) - r(1-r)P_{UVU}.
  $$
\end{lema}


Construction C8 needs special treatment.

\begin{lema}[\eliminationlemma] \label{lemma4.6}\label{lemma34}  % EL7 \quad -/-/L4.5
  Let $Y$ be introduced by (TRATIO Y P Q r). Then we have:
  
  $$
  S_{ABY}=S_{ABP} - \frac{r}{4}P_{PAQB}.
  $$
\end{lema}


\begin{lema}[\eliminationlemma] \label{lemma4.7}\label{lemma35}  % EL8 \quad -/-/L4.6
  Let $Y$ be introduced by (TRATIO Y P Q r). Then we have:
  
  $$
  P_{ABY}=P_{ABP} - 4rS_{PAQB}.
  $$
\end{lema}


\begin{lema}[\eliminationlemma] \label{lemma4.8}\label{lemma36}  % EL9 \quad -/-/L4.7
  Let $Y$ be introduced by (TRATIO Y P Q r). Then we have:
  
  $$
  P_{AYB}=P_{APB} + r^2P_{PQP} - 4r(S_{APQ} + S_{BPQ}).
  $$
\end{lema}


Now we consider how to eliminate points from the ratio of lengths.

\begin{lema}[\eliminationlemma] \label{lemma4.9}\label{lemma37} % EL10 \quad -/-/L4.8
  Let $Y$ be introduced by (INTER Y (LINE U V) (LINE P Q)). The we
  have:

  
  $$
  \frac{\overline{AY}}{\overline{CD}} = \left\{
    \begin{array}{lcl}
      \frac{S_{AUV}}{S_{CUDV}} & \ & \mbox{if $A$ is not on $UV$}\\
      \frac{S_{APQ}}{S_{CPDQ}} & \ & \mbox{otherwise}\\
    \end{array}\right.
  $$
\end{lema}




\begin{lema}[\eliminationlemma] \label{lemma4.10}\label{lemma38} % EL11 \quad -/-/L4.9
  Let $Y$ be introduced by (FOOT Y P U V). We assume $D\neq U$; otherwise
  interchange $U$ and $V$.

  
  $$
  \frac{\overline{AY}}{\overline{CD}} = \left\{
    \begin{array}{lcl}
      \frac{P_{PCAD}}{P_{CDC}} & \ & \mbox{if $A$ is on $UV$}\\
      \frac{S_{AUV}}{S_{CUDV}} & \ & \mbox{otherwise}\\
    \end{array}\right.
  $$
\end{lema}


\begin{lema}[\eliminationlemma] \label{lemma4.11}\label{lemma39} % EL12 \quad -/-/L4.10
  Let $Y$ be introduced by (PRATIO Y R P Q r). Then we have

  
  $$
  \frac{\overline{AY}}{\overline{CD}} = \left\{
    \begin{array}{lcl}
      \frac{\ratio{AR}{PQ} + r}{\ratio{CD}{PQ}} & \ & \mbox{if $A$ is on
        $RY$}\\ 
      \frac{S_{APRQ}}{S_{CPDQ}} & \ & \mbox{otherwise}\\
    \end{array}\right.
  $$
\end{lema}


\begin{lema}[\eliminationlemma] \label{lemma4.12}\label{lemma40} % EL13 \quad -/-/L4.11
  Let $Y$ be introduced by (TRATIO Y P Q r). Then we have

  
  $$
  \ratio{AY}{CD} = \left\{
    \begin{array}{lcl}
      \frac{P_{APQ}}{P_{CPDQ}} & \ & \mbox{if $A$ is on $PY$}\\ 
      \frac{S_{APQ} - \frac{r}{4}P_{PQP}}{S_{CPDQ}} & \ & \mbox{otherwise}\\
    \end{array}\right.
  $$
\end{lema}


\subsection{Table of Elimination Lemmas}
\label{sec:eliminationlemmas}

%\psset{unit=0.25cm}\tiny
\begin{center}
\begin{sideways}
    \begin{tabular}{|c||c|c|c|c|c|c|c|c|}\hline
      & &Construction & ndc & \multicolumn{5}{c|}{Elimination formulas} \\
      \hline
      &&&& $P_{AYB}$ & $\begin{array}{cc} P_{ABY} &
        P_{ABCY}\end{array}$ & $\begin{array}{cc} S_{ABY} &
        S_{ABCY}\end{array}$ & $\ratio{AY}{CD}$ &\barra $\ratio{AY}{BY}$\\
      \hline 
      1 & C7 &\input{c7euk} & \parbox{10em}{$U\not=V$, if
        $r=\frac{r1}{r2}$ then $r2\not=0$}  & EL\ref{lemma:EL6} &
      \multicolumn{2}{c|}{EL\ref{lemma:EL2}} &
      \multicolumn{2}{c|}{EL\ref{lemma:EL12}} \\ \hline  
      2 & C8 &\input{c8euk} & \parbox{10em}{$U\not=V$, if
        $r=\frac{r1}{r2}$ then $r2\not=0$} & EL\ref{lemma:EL9} &
      EL\ref{lemma:EL8} & EL\ref{lemma:EL7} & 
      \multicolumn{2}{c|}{EL\ref{lemma:EL13}} \\ \hline 
      3 & C41 &\input{c41euk} && EL\ref{lemma:EL5} &
      \multicolumn{2}{c|}{EL\ref{lemma:EL3}} & EL\ref{lemma:EL10} &
      EL\ref{lemma:EL1}\\ \hline 
      4 & C42 &\input{c42euk} & $U\not=V$ & EL\ref{lemma:EL5} &
      \multicolumn{2}{c|}{EL\ref{lemma:EL4}} &
      \multicolumn{2}{c|}{EL\ref{lemma:EL11}}\\ \hline\hline 
      &&&& A & B & C & D & E \\ \hline
      \multicolumn{9}{l}{\ } \\
      \multicolumn{9}{l}{C7 -- (PRATIO Y W U V r)}\\ 
      \multicolumn{9}{l}{C8 -- (TRATIO Y U V r)}\\ 
      \multicolumn{9}{l}{C41 -- (INTER Y (LINE U V) (LINE P Q))}\\ 
      \multicolumn{9}{l}{C42 -- (FOOT Y P U V)}\\ 
    \end{tabular}
\end{sideways}
\end{center}


\subsection{Free Points and the Algorithm}

For a geometry statement $S=(C_1,C_2,\ldots,C_m,(E,F))$, after eliminating
all the non-free points introduced by $C_i$ from $E$ and $F$ using the
lemmas in the preceding subsections, we obtain two rational expression
$E^\prime$ and $F^\prime$ in indeterminates, areas and Pythagoras differences of
{\em free points}. These geometric quantities are generally not
independent, e.g. for any four points $A$, $B$, $C$, and $D$ we have

$$
S_{ABC} = S_{ABD} + S_{ADC} + S_{DBC}
$$

We thus need to reduce $E^\prime$ and $F^\prime$ to expressions in independent
variables. To do that, we need the concept of area coordinates.

\begin{defs}[Area Coordinates] \label{def:areaCoord}\label{def9}
  Let $A$, $O$, $U$, and $V$ be four points such that  $O$, $U$, and
  $V$ are not collinear. The area coordinates of $A$ with respect to
  $OUV$ are

  $$
  x_A = \frac{S_{OUA}}{S_{OUV}},\quad y_A =
  \frac{S_{OAV}}{S_{OUV}},\quad z_A =  \frac{S_{AUV}}{S_{OUV}}.
  $$

It is clear that $x_A+y_A+z_A = 1$. Since $x_A$, $y_A$, and $z_A$ are
not independent, we also call $x_A$, $y_A$ the area coordinates of $A$
with respect to $OUV$.
\end{defs}

It is clear that the points in the plane are in a one to one
correspondence with their area coordinates. To represent $E$ and $F$
as expressions in independent variables, we first introduce three new
points $O$, $U$, and $V$, such that, $UO\perp OV$. We will reduce $E$ and
$F$ to expressions in the area coordinates of the free points with
respect to $OUV$.

For any free points $A$, $B$, and $C$, we have the following results.


\begin{lema}\label{lemma4.14.1}\label{lemma41} %[-/-/L4.13] 
  $S_{ABC} = \frac{(S_{OVB} - S_{OVC})S_{OUA} + (S_{OVC} -
    S_{OVA})S_{OUB} + (S_{OVA} - S_{OVB})S_{OUC}}{S_{OUV}}$.
\end{lema}

\begin{lema}\label{lemma4.14.2}\label{lemma42} %[-/-/L4.13]
  $P_{ABC} = \overline{AB}^2 + \overline{CB}^2 - \overline{AB}^2$
\end{lema}

\begin{lema}\label{lemma4.14.3}\label{lemma43} %[-/-/L4.13] 
  $\overline{AB}^2 = \frac{\overline{OU}^2(S_{OVA} -
    S_{OVB})^2}{S^2_{OUV}} + \frac{\overline{OV}^2(S_{OUA} -
    S_{OUB})^2}{S^2_{OUV}}$.
\end{lema}

\begin{lema} \label{lemma4.14.4}\label{lemma44} %\label{lemma41}
  $S^2_{OUV} = \frac{\overline{OU}^2\cdot\;\overline{OV}^2}{4}$.
\end{lema}

Using Lemma~\ref{lemma4.14.1} to~\ref{lemma4.14.4}, $E$ and $F$ can
be written as expressions in $\overline{OU}$, $\overline{OV}$, and the
area coordinates of the free points. Since the area coordinates of
free points are independent, $E=F$ iff $E$ and $F$ are literally the
same.


\subsection{The Area Algorithm}
\label{sec:areaAlg}


\begin{description}
\item[$\to$] $S=(C_1,C_2,\ldots,C_m,(E,F))$ is a statement in $\mathbf{C}$.
\item[$\gets$] The algorithm tells whether $S$ is true, or not, and if
  it is true, produces a proof for $S$.
\end{description}

\begin{verbatim}
for (i=m;i==1;i--) {
   if (the ndg conditions of Ci is satisfied) exit;
   // Let G1,\ldots,Gn be the geometric quantities in E and F
   for (j=1;j<=n,j++) {
      Hj <- eliminating the point introduced by construction Ci from Gj
      E <- E[Gj:=Hj]
      F <- F[Gj:=Hj]
   }
}
if (E==F) S <- true
else S<-false
\end{verbatim}

The ndg condition of a construction has three forms: $A\neq B$,
$PQ\nparallel UV$, or $PQ\notperp UV$. For the first case we check
if $P_{ABA} = 2\overline{AB}^2 = 0$. For the second case, we
check if $S_{PUV} = S_{QUV}$. For the third case, we check if $P_{PUV}
= P_{QUV}$. If a ndg condition of a geometry statement is not
satisfied, the statement is {trivially true}.

\vspace*{1em}
{\em Proof of the correctness.} Only the last step needs
explanation. If $E=F$, the statement is obviously true. Note that the
ndg condition ensure that the denominators of all the expressions
occurring in the proof do not vanish.

Otherwise, since the geometric quantities in $E$ and $F$ are all free
parameters, i.e., in the geometric configuration of $S$ they can take
arbitrary values. Since $E\neq F$, we can take some concrete values for
these quantities such that when replacing these quantities by the
corresponding values in $E$ and $F$, we obtain two different
numbers. In other words, we obtain a counter example for $S$.

\hfill q.e.d.
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "tech-rep02.tex"
%%% End: 