Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:evaluating_formulas_in_finite_structures [2008/03/19 00:37] vkuncak |
sav08:evaluating_formulas_in_finite_structures [2008/03/19 00:39] vkuncak |
||
---|---|---|---|
Line 22: | Line 22: | ||
List contains no duplicates: | List contains no duplicates: | ||
ALL n1. ALL n2. ListNode(n1) & ListNode(n2) & data(n1)=data(n2) --> n1=n2 | ALL n1. ALL n2. ListNode(n1) & ListNode(n2) & data(n1)=data(n2) --> n1=n2 | ||
+ | |||
===== Efficiency of Evaluating Formulas ===== | ===== Efficiency of Evaluating Formulas ===== | ||
- | Given a language ${\cal L}$, formula a formula $F$ in ${\cal L}$ and an interpretation $I=(D,\alplha)$, 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 formula: LOGSPACE (iterate over elements) | ||
* fix language with symbols of bounded arity: PSPACE (reduce to [[QBF and Quantifier Elimination|QBF]]) | * fix language with symbols of bounded arity: PSPACE (reduce to [[QBF and Quantifier Elimination|QBF]]) |