- English only
Lab for Automated Reasoning and Analysis LARA
Differences
This shows you the differences between the selected revision and the current version of the page.
| sav12:first-order_logic_with_sets_and_updates 2012/04/23 10:04 | sav12:first-order_logic_with_sets_and_updates 2012/04/23 10:05 current | ||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== First-Order Logic with Sets and Update Expressions ====== | ====== First-Order Logic with Sets and Update Expressions ====== | ||
| - | **Claim:** we can add update operations, a well as operations of set algebra on sets and relations to first-order logic. These constructs do not change expressive power and can be eliminated. Result are first-order logic formulas. | + | **Claim:** we can add update operations, a well as operations of set algebra on sets and relations to first-order logic. These constructs do not change the expressive power and can be eliminated. Result is a first-order logic formula. |
| Syntactic extension of FOL with if-then-else, function update, sets. | Syntactic extension of FOL with if-then-else, function update, sets. | ||