Unravelings and Ultra-properties
Unravelings and Ultra-properties
复制标题
解开和超属性
DOI：
10.1007/3-540-61735-3_7
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
M. Marchiori
中科院分区：
文献类型：
--
作者：
M. Marchiori
条件重写被公认为比无条件重写复杂得多。本文研究了从简单的无条件改写理论中可以自动推断出多少条件改写。我们引入了一种新的工具，称为拆解，将条件项重写系统（CTRS）自动转换为术语重写系统（TRS）。通过使用相应的TRS研究相应的超性质，展开可以推断CTRS的性质。我们展示了如何重新发现诸如减少之类的性质，并对ctrs上的一些现有结果给出了很好的证明。此外，我们还展示了展开如何为研究ctrs的模块化提供了一个有价值的工具，自动给出了大量新的结果。
Conditional rewriting is universally recognized as being much more complicated than unconditional rewriting. In this paper we study how much of conditional rewriting can be automatically inferred from the simpler theory of unconditional rewriting. We introduce a new tool, called unraveling, to automatically translate a conditional term rewriting system (CTRS) into a term rewriting system (TRS). An unraveling enables to infer properties of a CTRS by studying the corresponding ultra-properties using the corresponding TRS. We show how to rediscover properties like decreasingness, and to give nice proofs of some existing results on CTRSs. Moreover, we show how unravelings provide a valuable tool to study modularity of CTRSs, automatically giving a multitude of new results.