Simple Search

Query:

Enter a query and click »Search«...

Format:

Display: entries per page entries

Zbl 0678.68094
Kapur, Deepak
A refutational approach to geometry theorem proving. (English)
[J] Artif. Intell. 37, No.1-3, 61-93 (1988). ISSN 0004-3702

The paper under review is an interesting contribution to the very active field of automatic theorem proving initiated by Wu Wen Tsün's refinement of Descartes's method of algebraic geometry. A lot of geometric statements in affine or euclidean plane are amenable to mechanical proving provided that they are expressible as the emptiness of the algebraic set of zeros in the associated field K of a finite set of equations over the base field $k\subseteq K$. Taking K to be algebraically closed, the proposed approach is based on Hilbert's Nullstellensatz and is complete in Wu's geometry but, no wonder is incomplete, in Tarski's geometry. To get completeness in the latter case a real Nullstellensatz is more opportune. Unlike Wu's approach, the proposed approach uses the Gröbner basis method instead of the factorization of polynomials.
[S.B.Basarab]

MSC 2000:: *68T15 Theorem proving
14M99 Special varieties
68W30 Symbolic computation and algebraic computation
14N99 Classical algebraic geometry

Keywords: satisfiability; Nullstellensatz; Gröbner basis

Comment on this Item PDF MathML XML ASCII DVI PS BibTeX Online Ordering Article Journal

	Scientific prize winners of the ICM 2010
	Overhang
	Lie groups, physics and geometry. An introduction for physicists, engineers and chemists.

Simple Search

Zentralblatt MATH Berlin [Germany]