In algebraic geometry, elimination theory is the classical name for algorithmic approaches to eliminating between polynomials of several variables.

The linear case would now routinely be handled by Gauss-Jordan elimination, rather than the theoretical solution provided by Cramer's rule. In the same way, computational techniques for elimination can in practice be based on Gröbner basis methods. There is however older literature on types of eliminant, including resultants to find common roots of polynomials, discriminants and so on. Some of the systematic methods have a homological basis, that can be made explicit, as in Hilbert's theorem on syzygies. This field is at least as old as Bézout's theorem.

The historical development of commutative algebra, which was initially called ideal theory, is closely linked to concepts in elimination theory: ideas of Kronecker, who wrote a major paper on the subject, were adapted by Hilbert and effectively 'linearised' while dropping the explicit constructive content. The process continued over many decades: the work of F.S. Macaulay who gave his name to Cohen-Macaulay modules was motivated by elimination.

There is also a logical content to elimination theory, as seen in the Boolean satisfiability problem. In the worst case it is presumably hard to eliminate variables computationally. Elimination of quantifiers is a term used in mathematical logic to explain that in some cases - algebraic geometry of projective space over an algebraically closed field being one - existential quantifiers can be removed. The content of this, in the geometric case, is that an algebraic correspondence (i.e. Zariski-closed relation) between two projective spaces projects to a Zariski-closed set: the condition on x that x R y for some y is a polynomial condition on x. There is some historical evidence that this fact influenced Hilbert's thinking about the prospects for proof theory.