Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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)) 
  
 
sav08/qe_from_conjunction_of_literals_suffices.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice