Grammar Rewriting
We present a term rewriting procedure based on congruence closure that can be used with arbitrary equational theories. This procedure is motivated by the pragmatic need to prove equations in equational theories where confluence can not be achieved. The procedure uses context free grammars to...
| Autor principal: | |
|---|---|
| Lenguaje: | en_US |
| Publicado: |
2004
|
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/1721.1/5973 |
| _version_ | 1826210002805719040 |
|---|---|
| author | McAllester, David |
| author_facet | McAllester, David |
| author_sort | McAllester, David |
| collection | MIT |
| description | We present a term rewriting procedure based on congruence closure that can be used with arbitrary equational theories. This procedure is motivated by the pragmatic need to prove equations in equational theories where confluence can not be achieved. The procedure uses context free grammars to represent equivalence classes of terms. The procedure rewrites grammars rather than terms and uses congruence closure to maintain certain congruence properties of the grammar. Grammars provide concise representations of large term sets. Infinite term sets can be represented with finite grammars and exponentially large term sets can be represented with linear sized grammars. |
| first_indexed | 2024-09-23T14:39:32Z |
| id | mit-1721.1/5973 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T14:39:32Z |
| publishDate | 2004 |
| record_format | dspace |
| spelling | mit-1721.1/59732019-04-10T17:24:31Z Grammar Rewriting McAllester, David context free languages term rewriting Knuth-Bendixscompletion automated reasoning theorem proving equational reasoning We present a term rewriting procedure based on congruence closure that can be used with arbitrary equational theories. This procedure is motivated by the pragmatic need to prove equations in equational theories where confluence can not be achieved. The procedure uses context free grammars to represent equivalence classes of terms. The procedure rewrites grammars rather than terms and uses congruence closure to maintain certain congruence properties of the grammar. Grammars provide concise representations of large term sets. Infinite term sets can be represented with finite grammars and exponentially large term sets can be represented with linear sized grammars. 2004-10-04T14:24:26Z 2004-10-04T14:24:26Z 1991-12-01 AIM-1342 http://hdl.handle.net/1721.1/5973 en_US AIM-1342 21 p. 1916751 bytes 1510872 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | context free languages term rewriting Knuth-Bendixscompletion automated reasoning theorem proving equational reasoning McAllester, David Grammar Rewriting |
| title | Grammar Rewriting |
| title_full | Grammar Rewriting |
| title_fullStr | Grammar Rewriting |
| title_full_unstemmed | Grammar Rewriting |
| title_short | Grammar Rewriting |
| title_sort | grammar rewriting |
| topic | context free languages term rewriting Knuth-Bendixscompletion automated reasoning theorem proving equational reasoning |
| url | http://hdl.handle.net/1721.1/5973 |
| work_keys_str_mv | AT mcallesterdavid grammarrewriting |