• English only

# Differences

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

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 =====