On Role Logic
We present role logic, a notation for describing propertiesof relational structures in shape analysis, databases, andknowledge bases. We construct role logic using the ideas ofde Bruijn's notation for lambda calculus, an encoding offirst-order logic in lambda calculus, and a simple rule forimp...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30430 |
| _version_ | 1811088322747957248 |
|---|---|
| author | Kuncak, Viktor Rinard, Martin |
| author2 | Computer Architecture |
| author_facet | Computer Architecture Kuncak, Viktor Rinard, Martin |
| author_sort | Kuncak, Viktor |
| collection | MIT |
| description | We present role logic, a notation for describing propertiesof relational structures in shape analysis, databases, andknowledge bases. We construct role logic using the ideas ofde Bruijn's notation for lambda calculus, an encoding offirst-order logic in lambda calculus, and a simple rule forimplicit arguments of unary and binary predicates.The unrestricted version of role logic has the expressivepower of first-order logic with transitive closure. Using asyntactic restriction on role logic formulas, we identify anatural fragment RL^2 of role logic. We show that the RL^2fragment has the same expressive power as two-variable logicwith counting C^2 and is therefore decidable.We present a translation of an imperative language into thedecidable fragment RL^2, which allows compositionalverification of programs that manipulate relationalstructures. In addition, we show how RL^2 encodes booleanshape analysis constraints and an expressive descriptionlogic. |
| first_indexed | 2024-09-23T14:00:23Z |
| id | mit-1721.1/30430 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T14:00:23Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/304302019-04-12T08:26:06Z On Role Logic Kuncak, Viktor Rinard, Martin Computer Architecture We present role logic, a notation for describing propertiesof relational structures in shape analysis, databases, andknowledge bases. We construct role logic using the ideas ofde Bruijn's notation for lambda calculus, an encoding offirst-order logic in lambda calculus, and a simple rule forimplicit arguments of unary and binary predicates.The unrestricted version of role logic has the expressivepower of first-order logic with transitive closure. Using asyntactic restriction on role logic formulas, we identify anatural fragment RL^2 of role logic. We show that the RL^2fragment has the same expressive power as two-variable logicwith counting C^2 and is therefore decidable.We present a translation of an imperative language into thedecidable fragment RL^2, which allows compositionalverification of programs that manipulate relationalstructures. In addition, we show how RL^2 encodes booleanshape analysis constraints and an expressive descriptionlogic. 2005-12-22T01:12:11Z 2005-12-22T01:12:11Z 2003-10-24 MIT-CSAIL-TR-2003-025 MIT-LCS-TR-925 http://hdl.handle.net/1721.1/30430 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 20 p. 26284070 bytes 1140595 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Kuncak, Viktor Rinard, Martin On Role Logic |
| title | On Role Logic |
| title_full | On Role Logic |
| title_fullStr | On Role Logic |
| title_full_unstemmed | On Role Logic |
| title_short | On Role Logic |
| title_sort | on role logic |
| url | http://hdl.handle.net/1721.1/30430 |
| work_keys_str_mv | AT kuncakviktor onrolelogic AT rinardmartin onrolelogic |