Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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 =====
 
sav08/evaluating_formulas_in_finite_structures.txt · Last modified: 2008/03/19 15:23 by vkuncak
 
© EPFL 2018 - Legal notice