Quantifier elimination

Quantifier elimination

Quantifier elimination is a technique in mathematical logic, model theory, and theoretical computer science.We say that a given theory has quantifier elimination if for every sentence with quantification there exists an equivalent (modulo the theory) sentence without quantifiers.

In model theory, quantifier elimination has several alternative characterizations, and does not necessarily imply the existence of a quantifier elimination algorithm.

A quantifier elimination algorithm for a given theory transforms formulas with quantifiers into equivalent formulas without quantifiers.Using a quantifier elimination algorithm we can transform every sentence (formula with no free variables) into an equivalent formula with no variables, which can usually be decided by simple computation. Therefore, a quantifier elimination algorithm for a theory typically implies the decidability of the theory.

Examples of theories that have been shown decidable using quantifier elimination are Presburger arithmetic, real closed fields, atomless Boolean algebras, term algebras, dense linear orders, random graphs,Feature trees, as well as many of their combinations such as Boolean Algebra with Presburger arithmetic, and Term Algebras with Queues. Quantifier elimination can also be used to show that "combining" decidable theories leads to new decidable theories. Such constructions include Feferman-Vaught theorem and Term Powers.

Basic ideas

To show constructively that a theory has quantifier elimination, it suffices to show that we can eliminate an existential quantifier applied to a conjunction of literals, that is, show that each formula of the form:

:exists x. igwedge_{i=1}^n L_i

where each L_i is a literal, is equivalent to a quantifier-free formula. Indeed, suppose we know how to eliminate quantifiers from conjunctions of formulas, then if F is a quantifier-free formula, we can write it in disjunctive normal form

:igvee_{j=1}^m igwedge_{i=1}^n L_{ij},

and use the fact that

:exists x. igvee_{j=1}^m igwedge_{i=1}^n L_{ij}

is equivalent to

:igvee_{j=1}^m exists x. igwedge_{i=1}^n L_{ij}.

Finally, to eliminate a universal quantifier

:forall x. F

where F is quantifier-free, we transform lnot F into disjunctive normal form, and use the fact that forall x. Fis equivalent to lnot exists x. lnot F.

References

* Wilfrid Hodges. "Model Theory". Cambridge University Press. 1993.
* Viktor Kuncak and Martin Rinard. "Structural Subtyping of Non-Recursive Types is Decidable". In "Eighteenth Annual IEEE Symposium on Logic in Computer Science," 2003.


Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать курсовую

Look at other dictionaries:

  • Elimination des quantificateurs — Élimination des quantificateurs En algorithmique ou en logique mathématique, l élimination des quantificateurs est l action de remplacer une formule d une certaine logique contenant éventuellement des quantificateurs ∀ ou ∃ par une formule… …   Wikipédia en Français

  • Élimination des quantificateurs — En algorithmique ou en logique mathématique, l élimination des quantificateurs est l action consistant à remplacer une formule d une certaine logique contenant éventuellement des quantificateurs ∀ ou ∃ par une formule équivalente (admettant les… …   Wikipédia en Français

  • Fourier–Motzkin elimination — is a mathematical algorithm for eliminating variables from a system of linear inequalities. It can look for both real and integer solutions. It is computationally expensive.Elimination (or exists elimination) of variables V from a system of… …   Wikipedia

  • Model theory — This article is about the mathematical discipline. For the informal notion in other parts of mathematics and science, see Mathematical model. In mathematics, model theory is the study of (classes of) mathematical structures (e.g. groups, fields,… …   Wikipedia

  • Real closed field — In mathematics, a real closed field is a field F in which any of the following equivalent conditions are true:#There is a total order on F making it an ordered field such that, in this ordering, every positive element of F is a square in F and… …   Wikipedia

  • Corps réel clos — En mathématiques, un corps réel clos est un corps totalement ordonné F tel que tout élément positif soit un carré et que tout polynôme de degré impair à coefficients dans F ait au moins une racine dans F. Le corps des réels, le corps des réels… …   Wikipédia en Français

  • Mathematical logic — (also known as symbolic logic) is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic.[1] The field includes both the mathematical study of logic and the… …   Wikipedia

  • Corps Réel Clos — Un corps réel clos est un corps ordonné tel que tout élément positif soit un carré et que tout polynôme de degré impair à coefficients dans F ait au moins une racine dans F. Le corps des réels, le corps des réels calculables (au sens de Turing)… …   Wikipédia en Français

  • Corps reel clos — Corps réel clos Un corps réel clos est un corps ordonné tel que tout élément positif soit un carré et que tout polynôme de degré impair à coefficients dans F ait au moins une racine dans F. Le corps des réels, le corps des réels calculables (au… …   Wikipédia en Français

  • Differentially closed field — In mathematics, a differential field K is differentially closed if every finite system of differential equations with a solution in some differential field extending K already has a solution in K. This concept was introduced by Robinson (1959).… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”