Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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