Differences

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

--- sav08:evaluating_formulas_in_finite_structures [2008/03/19 00:39]
vkuncak
+++ sav08:evaluating_formulas_in_finite_structures [2008/03/19 15:23]
vkuncak
@@ Line 6: / Line 6: @@
 Then evaluation functions $e_F$ and $e_T$ give algorithms to determine the truth value of $F$.
+This is the model checking problem for first-order logic on finite structures: is a given interpretation model of $F$.
 ===== Applications of Formula Evaluation =====
@@ Line 22: / Line 25: @@
 List contains no duplicates:
   ALL n1. ALL n2. ListNode(n1) & ListNode(n2) & data(n1)=data(n2) --> n1=n2
 ===== Efficiency of Evaluating Formulas =====
 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]])
-===== References =====
+Basic idea: to evaluate quantifiers, iterate over all domain elements.
-  * Neil Immerman: Descriptive Complexity
+  * 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 =====
+  * [[http://citeseer.ist.psu.edu/burch90symbolic.html|Symbolic Model Checking: 10^20 States and Beyond]]
+  * Neil Immerman: Descriptive Complexity, Springer