On Generalized Records and Spatial Conjunction in Role Logic
We have previously introduced role logic as a notation fordescribing properties of relational structures in shapeanalysis, databases and knowledge bases. A natural fragmentof role logic corresponds to two-variable logic withcounting and is therefore decidable.We show how to use role logic to descri...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30457 |
| _version_ | 1811083977425944576 |
|---|---|
| author | Kuncak, Viktor Rinard, Martin |
| author2 | Computer Architecture |
| author_facet | Computer Architecture Kuncak, Viktor Rinard, Martin |
| author_sort | Kuncak, Viktor |
| collection | MIT |
| description | We have previously introduced role logic as a notation fordescribing properties of relational structures in shapeanalysis, databases and knowledge bases. A natural fragmentof role logic corresponds to two-variable logic withcounting and is therefore decidable.We show how to use role logic to describe open and closedrecords, as well the dual of records, inverse records. Weobserve that the spatial conjunction operation of separationlogic naturally models record concatenation. Moreover, weshow how to eliminate the spatial conjunction of formulas ofquantifier depth one in first-order logic with counting. Asa result, allowing spatial conjunction of formulas ofquantifier depth one preserves the decidability oftwo-variable logic with counting. This result applies totwo-variable role logic fragment as well.The resulting logic smoothly integrates type system andpredicate calculus notation and can be viewed as a naturalgeneralization of the notation for constraints arising inrole analysis and similar shape analysis approaches. |
| first_indexed | 2024-09-23T12:42:38Z |
| id | mit-1721.1/30457 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T12:42:38Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/304572019-04-11T06:23:25Z On Generalized Records and Spatial Conjunction in Role Logic Kuncak, Viktor Rinard, Martin Computer Architecture We have previously introduced role logic as a notation fordescribing properties of relational structures in shapeanalysis, databases and knowledge bases. A natural fragmentof role logic corresponds to two-variable logic withcounting and is therefore decidable.We show how to use role logic to describe open and closedrecords, as well the dual of records, inverse records. Weobserve that the spatial conjunction operation of separationlogic naturally models record concatenation. Moreover, weshow how to eliminate the spatial conjunction of formulas ofquantifier depth one in first-order logic with counting. Asa result, allowing spatial conjunction of formulas ofquantifier depth one preserves the decidability oftwo-variable logic with counting. This result applies totwo-variable role logic fragment as well.The resulting logic smoothly integrates type system andpredicate calculus notation and can be viewed as a naturalgeneralization of the notation for constraints arising inrole analysis and similar shape analysis approaches. 2005-12-22T01:26:10Z 2005-12-22T01:26:10Z 2004-04-06 MIT-CSAIL-TR-2004-016 MIT-LCS-TR-942 http://hdl.handle.net/1721.1/30457 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 30 p. 29046951 bytes 1214158 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Kuncak, Viktor Rinard, Martin On Generalized Records and Spatial Conjunction in Role Logic |
| title | On Generalized Records and Spatial Conjunction in Role Logic |
| title_full | On Generalized Records and Spatial Conjunction in Role Logic |
| title_fullStr | On Generalized Records and Spatial Conjunction in Role Logic |
| title_full_unstemmed | On Generalized Records and Spatial Conjunction in Role Logic |
| title_short | On Generalized Records and Spatial Conjunction in Role Logic |
| title_sort | on generalized records and spatial conjunction in role logic |
| url | http://hdl.handle.net/1721.1/30457 |
| work_keys_str_mv | AT kuncakviktor ongeneralizedrecordsandspatialconjunctioninrolelogic AT rinardmartin ongeneralizedrecordsandspatialconjunctioninrolelogic |