Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:evaluating_formulas_in_finite_structures [2008/03/19 10:41] vkuncak |
sav08:evaluating_formulas_in_finite_structures [2008/03/19 15:23] (current) vkuncak |
||
---|---|---|---|
Line 30: | Line 30: | ||
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)$. | ||
- | Basic idea: iterate over all domain elements for quantifiers. | + | Basic idea: to evaluate quantifiers, iterate over all domain elements. |
- | + | ||
- | * fix formula: LOGSPACE (number of vars fixed, number of their bits changes) | + | |
- | * fix language with symbols of bounded arity: PSPACE (number of variables increases with formula size, see also [[QBF and Quantifier Elimination|QBF]]) | + | |
+ | * 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 ===== |