Videos

On Protocols for the Automatic Discovery of Elementary Geometry Theorems

Presenter
May 30, 2007
Abstract
Joint work with work with G. Dalzotto and A. Montes. In the talk we will deal with automatic discovery of elementary geometry theorems, through the algebraic geometry framework that has already shown its success for automatic theorem proving. Automatic discovery of theorems addresses the case of statements that are false in most relevant cases. It aims to produce, automatically, complementary hypotheses for the given statement to become correct. For example, we can draw a triangle and, then, the feet of the corresponding altitudes. These feet are the vertices of a new triangle, the so called "orthic" triangle for the given triangle. We want this orthic triangle to be equilateral, but it is not so, in general. Thus we impose as a thesis that the orthic triangle is equilateral and we expect our method to find the more general situations in which this is going to happen. In the talk we do not start providing a method, but stating a general framework for discovery, a kind of general protocol. Namely, we begin collecting the conditions that a couple of ideals, each one belonging to different set of variables–ideally related to the degrees of freedom of the geometric situation–, should verify in order to express necessary and sufficient conditions for the given thesis to hold. Such couple of ideals (named here as a FSDIC) will contribute for some extra hypothesis of equality (respectively, of inequality) type that are required for the theorem to hold. It will be shown, through examples, that such couple does not always exist (and it is, in general, not unique). But, if it exists, then we can identify and construct a particular FSDIC, that turns out to be very close to the output of the method presented in Recio-Velez, Journal of Automated Reasoning, 23, (1999). A test for the existence of a FSDIC will be then stated. Next we will explore the meaning of FSDIC for wise choices of variables (ie. when we deal with "interesting" variables), but we will also remark its limitations in other contexts. We will show how the inclusion "a priori", as part of the hypotheses, of some non-degeneracy conditions, could help computing through the discovery protocol we are considering. And, then, we will observe how this inclusion can be done through two (apparently similar) methods, but that the choice of one or the other has, sometimes, different consequences and requires human decision. Finally we will exhibit a collection of examples achieved via different methods, including, in particular, the use of Montes' MCCGS (minimal canonical comprehensive Groebner basis), that yields some results surprisingly close to our geometric intuition.