A Decision Method for Elementary Algebra and Geometry

By A. Tarski. 2023

2,212 citations recorded by the source corpus.

By a decision method for a class K of sentence (or other expressions) is meant a method by means of which, given any sentence θ, one can always decide in a finite number of steps whether θ is in K; by a decision problem for a class K we mean the problem of finding a decision method for K. A decision method must be like a recipe, which tells one what to do at each steps so that no intelligence is required to follow it; and the method can be applied by anyone so long as he is able to read and follow directions.

Subfields: Computational Theory and Mathematics, Computer Networks and Communications, Management Science and Operations Research

View Paper: https://www.semanticscholar.org/paper/686812651628808e11f6fe661e681bc2a572c7da

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

In Computer Networks and Communications

In Management Science and Operations Research

Citations in the corpus

Completeness and Categoricity. Part I: Nineteenth-century Axiomatics to Twentieth-century Metalogic (2002, background): “8 Tarski 1951, compare also the discussion in van den Dries 1988.”
Undecidability of linear inequalities in graph homomorphism densities (2010, methodology): “ a rational point on which the polynomial takes a negative value will be found. The decidability of positivity of a polynomial with rational coeﬃcients follows also from the well-known work of Tarski [Tar48]. In the following theorem we show that the problem of determining the positivity of a quantu”
A survey of computational complexity results in systems and control (2000, methodology): “a correction appears in Tsitsiklis and Blondel (1997b). (1997). It turns out however that the slightly di!erent problem of deciding whether o6 41 (as well as the question of boundedness of the set of all matrix products) is undecidable (Blondel and Tsitsiklis, 1999b).”
Algorithms in real algebraic geometry (2003, background): “The former proofs of quantifier elimination [152, 144, 44, 89] were effective, but the complexity of the associated algorithm was primitive recursive, and not elementary recursive.”
UNDECIDABLE PROBLEMS: A SAMPLER (2012, methodology): “this, one should restrict the input to have coecients in Q or in the eld R \Q of real algebraic numbers, so that the polynomial admits a nite encoding suitable for a Turing machine). In fact, Tarski [Tar51] gave a decision procedure, based on elimination of quantiers for R in the language of ordered”
QEPCAD B: a program for computing with semi-algebraic sets using CADs (2003, methodology): “The first procedure was invented by Alfred Tarski in the 1930s [21].”
Beyond Bell's theorem: correlation scenarios (2012, background): “her words, it boils down to deciding whether a given system of polynomial inequalities, containing the p(v1,...,vn) as parameters, has a solution over R. Thanks to Tarski’s real quantiﬁer elimination [Tar51], this system of polynomial inequalities is solvable if and only if p(v1,...,vn) itself satis”
A Combinatorial Approach to Nonlocality and Contextuality (2012, methodology): “Thanks to real quantifier elimination [93], there are known algorithms for doing this.”
On the Bennett–Hoeffding inequality (2009, background): “of G̃(a, b, t), based in essence on a theory by Tarski [53, 31, 14], can be found in the mentioned paper [35].”
The linear separability problem: some testing methods (2006, methodology): “Other methods for testing linear separability include the Tarski elimination algorithm [30] which verifies the validity of a special first order formula in an algebraic closed field”
Quantifier Elimination and Cylindrical Algebraic Decomposition (2004, methodology): “Tarski in 1948, (Tarski 1951) published a quantifier elimination method for the elementary theory of real closed fields (which he had discovered in 1930).”