Differences

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

--- sav08:evaluating_formulas_in_finite_structures [2008/03/18 19:12]
vkuncak
+++ sav08:evaluating_formulas_in_finite_structures [2008/03/19 00:45]
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 14: / Line 17: @@
 === Example: Checking Database Integrity Constraint ===
+Database integrity constraint:
+  ALL studentID. ALL courseID. Registered(studentID,courseID) --> (EX courseName. courseCatalog(courseID, courseName))
 === Example: Checking Assertion in Program with Heap ===
-=== Example: Checking Program Designs ===
+List contains no duplicates:
+  ALL n1. ALL n2. ListNode(n1) & ListNode(n2) & data(n1)=data(n2) --> n1=n2
 ===== Efficiency of Evaluating Formulas =====
-  * Neil Immerman: Descriptive Complexity
+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 =====
+  * [[http://citeseer.ist.psu.edu/burch90symbolic.html|Symbolic Model Checking: 10 20 States and Beyond]]
+  * Neil Immerman: Descriptive Complexity, Springer