Mechanical geometry theorem proving based on Gröbner bases

DOI10.1007/BF02943140MaRDI QIDQ676849zbMATH OpenOpenAlexFDO

Publication date 17 February 1998

Published in Journal of Computer Science and Technology (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf02943140

Gröbner bases mechanical theorem proving

Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Symbolic computation and algebraic computation (68W30)

Review text

The paper proposes a method for mechanical elementary geometry theorem proving. In more details, suppose a geometric statement is described by some polynomials \[ h_1,\ldots,h_m \in {\mathbb{Q}}[x_1,\ldots,x_n] \] and suppose the conclusion is expressed by a polynomial \(g\in {\mathbb{Q}}[x_1,\ldots,x_n]\); assume the ideal \(J=(h_1,\ldots,h_m)\) is zero-dimensional. The statement is said generally true if \(g\in \sqrt J\) and, if \({\mathcal M}\) is a minimal prime over \(J\), is said generally true on the component \(\mathcal M\) if \(g\in {\mathcal M}\). The paper gives an algorithm which computes, from the Gröbner basis of \(J\) with respect to a pure lexicographic order, the minimal primes over \(J\). In this way the author gives a method which allows to verify if a statement is generally true or generally true on some components of the ideal \(J\).

Recommendations

Cites work

Cited in

(16)

This page was built for publication: Mechanical geometry theorem proving based on Gröbner bases

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q676849)