Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:evaluating_formulas_in_finite_structures [2008/03/19 00:45] vkuncak |
sav08:evaluating_formulas_in_finite_structures [2008/03/19 15:23] vkuncak |
||
|---|---|---|---|
| Line 29: | Line 29: | ||
| Given a language ${\cal L}$, formula a formula $F$ in ${\cal L}$ and an interpretation $I=(D,\alpha)$, determine $e_F(F)(I)$. | Given a language ${\cal L}$, formula a formula $F$ in ${\cal L}$ and an interpretation $I=(D,\alpha)$, determine $e_F(F)(I)$. | ||
| - | * fix formula: LOGSPACE (iterate over elements) | + | |
| - | * fix language with symbols of bounded arity: PSPACE (reduce to [[QBF and Quantifier Elimination|QBF]]) | + | Basic idea: to evaluate quantifiers, iterate over all domain elements. |
| + | |||
| + | * fix formula, change domain size $|D|$: LOGSPACE (number of vars fixed, number of their bits changes) | ||
| + | * fix language with symbols of bounded arity, change formula: PSPACE (number of variables increases with formula size, see also [[QBF and Quantifier Elimination|QBF]]) | ||
| ===== References ===== | ===== References ===== | ||
| - | * [[http://citeseer.ist.psu.edu/burch90symbolic.html|Symbolic Model Checking: 10 20 States and Beyond]] | + | * [[http://citeseer.ist.psu.edu/burch90symbolic.html|Symbolic Model Checking: 10^20 States and Beyond]] |
| * Neil Immerman: Descriptive Complexity, Springer | * Neil Immerman: Descriptive Complexity, Springer | ||
| | | ||