Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:qbf_and_quantifier_elimination [2008/03/10 11:16] vkuncak |
sav08:qbf_and_quantifier_elimination [2008/03/11 16:14] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== QBF and Quantifier Elimination ====== | ====== QBF and Quantifier Elimination ====== | ||
- | === Quantified Propositional Formula Syntax === | + | ===== Quantified Propositional Formula Syntax ===== |
We extend the definition of formulas with quantifiers $\forall p.F$ and $\exists p.F$ where $p \in V$: | We extend the definition of formulas with quantifiers $\forall p.F$ and $\exists p.F$ where $p \in V$: | ||
Line 10: | Line 10: | ||
\] | \] | ||
- | === Eliminating quantifiers by expansion === | + | ===== Eliminating quantifiers by expansion ===== |
We can apply the following rules to eliminate propositional quantifiers: | We can apply the following rules to eliminate propositional quantifiers: | ||
Line 23: | Line 23: | ||
Notion of quantifier elimination applies to other logic as well. | 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 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. | + | **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. | + | **Observation:** 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. | + | **Observation:** 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: | In general QBF formulas can have alternations between $\forall$ and $\exists$ quantifiers: | ||
Line 36: | Line 36: | ||
\] | \] | ||
- | === Quantified Propositional Formula Semantics === | + | ===== Quantified Propositional Formula Semantics ===== |
- | We can similarly provide semantic function definition for propositional logic. | + | We can similarly provide recursive semantic function definition for propositional logic. |
- | === Notes on Computational Complexity === | + | ===== Summary of Computational Complexity of Problems ===== |
* checking satisfiability of propositional formula $F$ is NP-complete | * checking satisfiability of propositional formula $F$ is NP-complete |