% Abstrat of your communication to the
% ACA2018 Conference (Santiago de Compostela, 2018).
% You must use LaTeX format.


%====================================================
% IMPORTANT: DO NOT MODIFY THE FOLLOWING LINES
%====================================================

\documentclass{article}

\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{amssymb,amsthm,amsmath,amsfonts,latexsym}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{times}

\setlength{\oddsidemargin}{1.46cm}
\setlength{\textwidth}{13cm}
\setlength{\topmargin}{0.0cm}
\setlength{\textheight}{20.5cm}

\makeatletter
\newcommand{\TITLE}[2][]{
  \begin{center} \Large \bfseries #2%
  \def\@temp{#1}\ifx\@temp\@empty\relax\else\footnote{#1}\fi\end{center}}

\newcommand{\AUTHOR}[2][]{\textbf{#2}%
  \def\@temp{#1}\ifx\@temp\@empty\relax\else\textsuperscript{#1}\fi}

\newcommand{\ADDRESS}[2]{\noindent
  \textsuperscript{#1}\parbox[t]{0.9\textwidth}{#2} \vspace{6pt}}

\makeatother

\newcommand{\KEYWORDS}[1]{\paragraph{Keywords:} #1}
\newcommand{\MSCLASSIFICATION}[1]{\paragraph{Mathematics Subject Classification 2010:} #1}

\renewcommand{\thefootnote}{\fnsymbol{footnote}}
\setcounter{footnote}{0}
\pagestyle{empty}

\newcommand{\HEADING}{
{\noindent \small Applications of Computer Algebra -- ACA2018 \\
Santiago de Compostela, June 18--22, 2018} \vspace{10pt}}

%===============================================
% DO NOT MODIFY THE ABOVE LINES
%===============================================

\begin{document}

\HEADING


\TITLE[Partially supported by the Spanish Research Project MTM2017-88796-P
Computación simbólica: nuevos retos en álgebra y geometría y sus aplicaciones]{Detecting truth,  just on parts, in automated reasoning in geometry}

% Write the author names. Identify each one of them with a number
% in order to give their own affiliations later on.
\begin{center}
 \AUTHOR[1]{Zoltán Kovács},
 \AUTHOR[2]{Tomás Recio} and
 \AUTHOR[3]{\underline{M. Pilar Vélez}}
\end{center}


% Write now the abstract of your communication.

We introduce and discuss,  through a computational algebraic geometry approach, the automatic reasoning handling of propositions that are simultaneously true and false over some relevant collections of instances.  A rigorous, algorithmic criterion is presented for detecting such cases,  and its performance is exemplified through the implementation of this test on the dynamic geometry program \textit{GeoGebra}.

The algebraic geometry approach to automated reasoning in geometry proceeds by translating a geometric statement $\{H\Rightarrow T\}$ into polynomial expressions, after adopting a coordinate system. Then, the geometric instances verifying the hypotheses  can be represented as the solution of a system of polynomial equations $V(H)=\{h_1=0,\dots,h_r=0\}$ (\emph{hypotheses variety}) they are represented algebraically by the ideal (of hypotheses) $H=\left<h_1=0,\dots,h_r=0\right>$ generated by such polynomials. Analogously, the thesis is represented as the solution of a polynomial
 $V(T)=\{f=0\}$,  describing the hypotheses (resp.~the thesis) variety. 

Thus, when $V(H) \subseteq V(T)$ we can say that the theorem is \emph{always true}. But this fact rarely happens, even for well established theorems, because the algebraic translation of the geometric construction described by the hypotheses usually forgets explicitly excluding some  degenerate cases, cf.~\cite{DR}.

Thus, a delicate, but more useful,  approach for automated reasoning consists in exhibiting, first, a collection of independent variables modulo $H$, so that no polynomial relation among them holds over the whole $V(H)$ (\emph{independent variables modulo $H$}).  Now, the irreducible components of $V(H)$ where these variables do  remain independent are assumed to describe \emph{non-degenerate} instances.

 Accordingly,  a statement is called \emph{generally true} if the thesis holds, at least, over all the non-degenerate components. 
On the other hand, if over each non-degenerate component the thesis does not identically vanish, the statement is labeled as \emph{generally false}. Remark that this last includes the \emph{always false} case, where the thesis does not hold at all. A more detailed description of this quite established terminology (with small variants) can be consulted, for instance, at \cite{RV99}, \cite{CLS} or \cite{ZWS}.   It follows from the definition that  to be generally true and to be generally false are incompatible.  

However---and this is the object of interest in this talk---there are statements which happen to be,  simultaneously, not generally true and not generally false, i.e.~statements that are \emph{true, just on some components}. Recently, in \cite{ZWS}, a new terminology to describe such cases  has been introduced, labelling as \emph{generally true on components} or, simply,  as \emph{true on components}; moreover \cite{ZWS} presents an algorithmic test to check this property. We have decided---for the better comprehension of this notion by general users of dynamic geometry programs implementing this feature, such as {\it GeoGebra}---to label such statements in a more colloquial way, as  statements \emph{true on parts, false on parts}, in some specific sense we will describe in detail below. 
 
Let us first start analyzing a simple example. Consider  points $A (0,0), B (2,0)$ in the plane and construct circles $c= (x-0)^2+(y-0)^2-3$ and $d=(x-2)^2+(y-0)^2-3$, i.e.~circle $c$ is centered at $A$ and circle $d$ is centered at $B$ and both have the same radius $r=\sqrt 3$.  Finally, we consider the two points of intersection of these circles, namely, $E (u, v)$ and $F (m, n)$. Thus, the hypotheses ideal is 
 $\left< u^2+v^2-3,(u-2)^2+v^2-3,  m^2+n^2-3, (m-2)^2+n^2-3\right>.$
 
 The thesis states the parallelism of the lines $AE$ and $BF$, that is, the vanishing of the polynomial
 $u\cdot n-v\cdot(m-2).$
 \noindent The ideal of hypotheses is clearly zero-dimensional, so there are no independent variables, nor degenerate components. Its primary components, over the rationals, are
\begin{center}
$\left<v-n, (m-2)^2+n^2-3, (u-2)^2+v^2-3, m^2+n^2-3, u^2+v^2-3\right>$\\
$\left<v+n, (m-2)^2+n^2-3, (u-2)^2+v^2-3, m^2+n^2-3, u^2+v^2-3\right>$.
\end{center}  
  It easy to check that the thesis is false over the first one and true over the second. This a clear, simple example of a neither true nor false, i.e. of a  \emph{true on components}, statement arising in an elementary geometry context (see other, less artificial examples in \cite{RV99,BR}).
  
 Obviously, since the idea of \emph{true on components}, or \emph{true on parts, false on parts}, is based on the concepts of degeneracy and of irreducible component, it follows that both the choice of the field over which the prime decomposition is performed (for example, the ideal $ H $ of the previous example has four components instead, if  
  $\mathbb{Q}(\sqrt{2})$ is considered as base field) and the choice of the independent variables --which determine which components are to be considered as degenerate-- could be essential. 
 
  
  About this last issue we would like to remark that when dealing with geometric statements it seems logical to take as independent variables the coordinates of the free points in the geometric construction we are dealing with; and we expect that its cardinality is the dimension of the hypotheses ideal. In most cases this ``intuitively'' maximal set of independent variables is maximum-size, but there are examples in which the coordinates of the free points in the geometric construction do not provide a maximum-size set of independent variables. See,  for instance,  Example 7 in \cite{DR}, concerning Euler's formula regarding the radii of the inner and outer circles of a triangle with vertices $(-1,0),(1,0), (u[1],u[2])$. Here the dimension of the hypotheses variety is expected to be 2 (referring to the two coordinates of the only free vertex of the triangle), but applying the algebraic definition of independence it turns out to be three\dots , unless it is explicitly required, and added as a  new hypothesis, that $(u[1],u[2])$ does not lie in the $x$-axis! This is a quite common problem---related, as mentioned above, to the difficult  \emph{a priori} control and detail of all geometric degeneracies---and is already considered in the basic reference of \cite{Chou}.  
  
 
The aim of this talk is to justify the specific interest of statements that, according to our terminology,  are simultaneously \emph{true on parts, false on parts} statements in the context of automated reasoning in geometry,  pointing out the subtle, involved, issues deriving from the  quirky algebraic behavior described in some of the examples above, as well as  exhibiting a new,  simpler way,  of testing if a statement is true and false on parts, by just detecting if a pair of elimination ideals are zero or not. This test has been implemented in the dynamic geometry software GeoGebra and some  illustrative examples can be found in \url{https://www.geogebra.org/m/zpDq7taB}. 
  
This extended abstract is  based on a recent work by the authors  \cite{KRV}.


% Write the keywords separated by commas

\KEYWORDS{geometry theorem proving and discovery, elementary geometry, Gr\"obner basis, elimination, true on components, GeoGebra}

% Write the MSC2010 codes corresponding to your communication

\MSCLASSIFICATION{13P10, 68T15}



% Next include the references you need.
% If your abstract includes no references at all, please delete all the lines
% from \begin{thebibliography} to \end{thebibliography}.

% Please, do not use more than 9 references.

\begin{thebibliography}{9}
\bibitem{BR}
\textsc{F. Botana and T. Recio}, On the unavoidable uncertainty of truth in dynamic geometry proving, \emph{Mathematics in Computer Science} \textbf{10} (1), 5-25 (2016).

\bibitem{Chou}
\textsc{S.C. Chou}, \emph{Mechanical geometry theorem proving}, Mathematics and its
  Applications (41), D. Reidel Publishing Co., Dordrecht (1988).
  
  \bibitem{CLS}
\textsc{D.A. Cox, J. Little and D. O'Shea}, \emph{Ideals, varieties, and algorithms. An
  introduction to computational algebraic geometry and commutative algebra}, 4th
  revised ed. Undergraduate Texts in Mathematics, Springer International Publishing, Switzerland (2015).

\bibitem{DR}
\textsc{G. Dalzotto and T. Recio}, On protocols for the automated discovery of theorems in elementary geometry, \emph{Journal of Automated Reasoning} \textbf{43}, 203-236 (2009).
  
%\bibitem{Tutorial}
%\textsc{Z. Kov\'acs,  T. Recio and  M.P. V\'elez}, GeoGebra automated reasoning tools: a tutorial. Available at
%https://github.com/kovzol/gg-art-doc/blob/master/pdf/english.pdf 

\bibitem{KRV}
\textsc{Z. Kov\'acs,  T. Recio and  M.P. V\'elez}, \textit{Detecting truth,  just on parts}, Preprint: arXiv: 1802.05875  [cs.AI] (2018).

\bibitem{RV99}
\textsc{T. Recio and  M.P. V\'elez},  Automatic discovery of theorems in elementary geometry, \emph{Journal of Automated Reasoning} \textbf{23}, 3-82 (1999).

\bibitem{ZWS}
\textsc{J. Zhou, D. Wang and Y. Sun},  Automated reducible geometric theorem proving and discovery by Gr\"obner basis method, \emph{Journal of Automated Reasoning}  \textbf{59} (3), 331-344 (2017).

  
\end{thebibliography}

\vspace{1cm}

% Full Affiliation of all authors
\ADDRESS{1}{
Private P\"adagogische Hochschule der Di\"ozese Linz \\
Salesianumweg 3, 4020 Linz \\
\texttt{zoltan@geogebra.org}
}

\vspace{.5cm}

\ADDRESS{2}{
Universidad de Cantabria \\
Avda. de los Castros, s/n, 39005 Santander (Spain) \\
\texttt{tomas.recio@unican.es}
}
\vspace{.5cm}

\ADDRESS{3}{
Universidad Antonio de Nebrija \\
C/ Pirineos, 55, 28040 Madrid (Spain) \\
\texttt{pvelez@nebrija.es}
}

\end{document}
