LARA

Differences

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

Link to this comparison view

sav08:qbf_and_quantifier_elimination [2008/03/10 11:17]
vkuncak 		sav08:qbf_and_quantifier_elimination [2015/04/21 17:30]
Line 1: Line 1:
-====== QBF and Quantifier Elimination ====== 
- 
-=== Quantified Propositional Formula Syntax === 
- 
-We extend the definition of formulas with quantifiers $\forall p.F$ and $\exists p.F$ where $p \in V$: 
-\[\begin{array}{rcl} 
-   ​F ​ & ::= & V \mid {\it false} \mid {\it true} \mid (F \land F) \mid (F \lor F) \mid (\lnot F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\ 
-      & \mid & \forall V. F\ \mid\ \exists V. F 
-\end{array} 
-\] 
- 
-=== Eliminating quantifiers by expansion === 
- 
-We can apply the following rules to eliminate propositional quantifiers:​ 
-\[ 
-    \exists p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \lor subst(\{p \mapsto {\it true}\},F) 
-\] 
-\[ 
-    \forall p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \land subst(\{p \mapsto {\it true}\},F) 
-\] 
-Note that the expansion can produce exponentially larger formula. 
- 
-Notion of quantifier elimination applies to other logic as well. 
- 
-Definition: A logic has //​quantifier elimination//​ if for every formula in the logic, there exists an equivalent formula without quantifiers. 
- 
-Definition: A quantifier elimination algorithm is an algorithm that takes a formula in a logic and converts it into an equivalent formula without quantifiers. 
- 
-Note: Formula $F$ is valid iff $\forall p_1,​\ldots,​p_n. F$ is true. 
- 
-Note: Formula $F$ is satisfiable iff $\exists p_1,​\ldots,​p_n. F$ is true. 
- 
-In general QBF formulas can have alternations between $\forall$ and $\exists$ quantifiers:​ 
-\[ 
-   ​\forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r)) 
-\] 
- 
-=== Quantified Propositional Formula Semantics === 
- 
-We can similarly provide recursive semantic function definition for propositional logic. 
- 
-=== Notes on Computational Complexity === 
- 
-  * checking satisfiability of propositional formula $F$ is NP-complete 
-  * checking validity of propositional formula $F$ is coNP-complete 
-  * checking truth value of arbitrary QBF formula is PSPACE-complete