Quantifier Elimination - Basic Ideas

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:

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

and use the fact that

is equivalent to

Finally, to eliminate a universal quantifier

where is quantifier-free, we transform into disjunctive normal form, and use the fact that is equivalent to

Read more about this topic:  Quantifier Elimination

Famous quotes containing the words basic and/or ideas:

    I fly in dreams, I know it is my privilege, I do not recall a single situation in dreams when I was unable to fly. To execute every sort of curve and angle with a light impulse, a flying mathematics—that is so distinct a happiness that it has permanently suffused my basic sense of happiness.
    Friedrich Nietzsche (1844–1900)

    A man of sense, though born without wit, often lives to have wit. His memory treasures up ideas and reflections; he compares them with new occurrences, and strikes out new lights from the collision. The consequence is sometimes bons mots, and sometimes apothegms.
    Horace Walpole (1717–1797)