- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

This shows you the differences between two versions of the page.

sav08:qe_from_conjunction_of_literals_suffices [2009/04/21 19:04] vkuncak |
sav08:qe_from_conjunction_of_literals_suffices [2015/04/21 17:30] (current) |
||
---|---|---|---|

Line 1: | Line 1: | ||

====== Quantifier Elimination from Conjunction of Literals is Sufficient ====== | ====== Quantifier Elimination from Conjunction of Literals is Sufficient ====== | ||

- | 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 [[wp>literal (mathematical logic)|literal]]s, that is, show that each formula of the form: | + | ((taken from [[wp>Quantifier Elimination]] to which it was originally contributed, so the Wikipedia sharing rights apply))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 [[wp>literal (mathematical logic)|literal]]s, that is, show that each formula of the form: |

- | \[ | + | \begin{equation*} |

\exists x. \bigwedge_{i=1}^n L_i | \exists x. \bigwedge_{i=1}^n L_i | ||

- | \] | + | \end{equation*} |

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 formulae, then if $F$ is a quantifier-free formula, we can write it in [[wp>disjunctive normal form]] | 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 formulae, then if $F$ is a quantifier-free formula, we can write it in [[wp>disjunctive normal form]] | ||

- | \[ | + | \begin{equation*} |

\bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij} | \bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij} | ||

- | \] | + | \end{equation*} |

and use the fact that | and use the fact that | ||

- | \[ | + | \begin{equation*} |

\exists x. \bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij} | \exists x. \bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij} | ||

- | \] | + | \end{equation*} |

is equivalent to | is equivalent to | ||

- | \[ | + | \begin{equation*} |

\bigvee_{j=1}^m \exists x. \bigwedge_{i=1}^n L_{ij} | \bigvee_{j=1}^m \exists x. \bigwedge_{i=1}^n L_{ij} | ||

- | \] | + | \end{equation*} |

Finally, to eliminate a universal quantifier | Finally, to eliminate a universal quantifier | ||

- | \[ | + | \begin{equation*} |

\forall x. F | \forall x. F | ||

- | \] | + | \end{equation*} |

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

- | |||

- | ((taken from [[wp>Quantifier Elimination]] to which it was originally contributed, so the Wikipedia sharing rights apply)) | ||