Detecting truth, just on parts (Q2425054)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Detecting truth, just on parts |
scientific article |
Statements
Detecting truth, just on parts (English)
0 references
26 June 2019
0 references
This article deals with a particular situation in automatic geometry theorem proving via computational algebraic geometry where a statement is neither generally true nor generally false but ``true on parts, false on parts'': It holds on some non-degenerate components while it is false on others. \par Instances of ``true on parts, false on parts'' occur typically in statements that involve a choice in a geometric construction, like selecting one of two intersection points of a circle with a line or one of two equilateral triangles over a line segment. The general concept is quite subtle and may depend on (a) the particular construction of a geometric object, (b) the selection of independent variables, and (c) the base field over which prime decomposition is performed. The authors prove that (c) is in fact irrelevant (Corollary~1). As to (b), they emphasize the role of \textit{maximal-size sets of independent variables}. Presuming that a problem be parameterized via such a set, a (computationally simple) criterion for ``true on parts, false on parts'' [\textit{T. Recio} and \textit{M. P. Vélez}, J. Autom. Reasoning 23, No. 1, 63--82 (1999; Zbl 0941.03010)] is equivalent to a (computationally more expensive) criterion that was proved under some stronger assumptions in [\textit{J. Zhou} et al., J. Autom. Reasoning 59, No. 3, 331--344 (2017; Zbl 1425.68383)]. \par The authors illustrate their findings at hand of several examples and also describe the implementation of their theory in recent version of \textit{GeoGebra}.
0 references
automatic deduction in geometry
0 references
automatic geometry theorem proving
0 references
Gröbner basis
0 references
zero divisor
0 references
true on parts
0 references
false on parts
0 references
true on components
0 references
dynamic geometry
0 references
0 references