Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:evaluating_formulas_in_finite_structures [2008/03/18 19:12] vkuncak |
sav08:evaluating_formulas_in_finite_structures [2008/03/19 00:46] vkuncak |
||
---|---|---|---|
Line 6: | Line 6: | ||
Then evaluation functions $e_F$ and $e_T$ give algorithms to determine the truth value of $F$. | 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 ===== | ===== Applications of Formula Evaluation ===== | ||
Line 14: | Line 17: | ||
=== Example: Checking Database Integrity Constraint === | === 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 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 ===== | ===== 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 | ||
+ | |