On Relational Analysis of Algebraic Datatypes
We present a technique that enables the use of finite modelfinding to check the satisfiability of certain formulaswhose intended models are infinite. Such formulas arisewhen using the language of sets and relations to reasonabout structured values such as algebraic datatypes. Thekey idea of our te...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30534 |
| _version_ | 1826206169553698816 |
|---|---|
| author | Kuncak, Viktor Jackson, Daniel |
| author2 | Computer Architecture |
| author_facet | Computer Architecture Kuncak, Viktor Jackson, Daniel |
| author_sort | Kuncak, Viktor |
| collection | MIT |
| description | We present a technique that enables the use of finite modelfinding to check the satisfiability of certain formulaswhose intended models are infinite. Such formulas arisewhen using the language of sets and relations to reasonabout structured values such as algebraic datatypes. Thekey idea of our technique is to identify a natural syntacticclass of formulas in relational logic for which reasoningabout infinite structures can be reduced to reasoning aboutfinite structures. As a result, when a formula belongs tothis class, we can use existing finite model findingtools to check whether the formula holds in the desiredinfinite model. |
| first_indexed | 2024-09-23T13:25:11Z |
| id | mit-1721.1/30534 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T13:25:11Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/305342019-04-11T06:23:24Z On Relational Analysis of Algebraic Datatypes Kuncak, Viktor Jackson, Daniel Computer Architecture We present a technique that enables the use of finite modelfinding to check the satisfiability of certain formulaswhose intended models are infinite. Such formulas arisewhen using the language of sets and relations to reasonabout structured values such as algebraic datatypes. Thekey idea of our technique is to identify a natural syntacticclass of formulas in relational logic for which reasoningabout infinite structures can be reduced to reasoning aboutfinite structures. As a result, when a formula belongs tothis class, we can use existing finite model findingtools to check whether the formula holds in the desiredinfinite model. 2005-12-22T02:25:50Z 2005-12-22T02:25:50Z 2005-04-05 MIT-CSAIL-TR-2005-022 MIT-LCS-TR-985 http://hdl.handle.net/1721.1/30534 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 13 p. 21208035 bytes 893051 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Kuncak, Viktor Jackson, Daniel On Relational Analysis of Algebraic Datatypes |
| title | On Relational Analysis of Algebraic Datatypes |
| title_full | On Relational Analysis of Algebraic Datatypes |
| title_fullStr | On Relational Analysis of Algebraic Datatypes |
| title_full_unstemmed | On Relational Analysis of Algebraic Datatypes |
| title_short | On Relational Analysis of Algebraic Datatypes |
| title_sort | on relational analysis of algebraic datatypes |
| url | http://hdl.handle.net/1721.1/30534 |
| work_keys_str_mv | AT kuncakviktor onrelationalanalysisofalgebraicdatatypes AT jacksondaniel onrelationalanalysisofalgebraicdatatypes |