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/19 00:39] 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 22: | Line 25: | ||
| 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 ===== | ||
| Line 33: | Line 34: | ||
| ===== References ===== | ===== References ===== | ||
| - | * Neil Immerman: Descriptive Complexity | + | * [[http://citeseer.ist.psu.edu/burch90symbolic.html|Symbolic Model Checking: 10^20 States and Beyond]] |
| + | * Neil Immerman: Descriptive Complexity, Springer | ||
| + | |||