Matchbox: A Tool for Match-Bounded String Rewriting
Matchbox: A Tool for Match-Bounded String Rewriting
复制标题
Matchbox：用于匹配限制字符串重写的工具
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Johannes Waldmann
中科院分区：
文献类型：
--
作者：
Johannes Waldmann
程序 Matchbox 相对于（反向）匹配范围字符串重写系统实现了常规语言的后代集合和非终止字符串集合的精确计算。 Matchbox 可以搜索给定重写系统及其一些转换变体的匹配高度属性的布尔组合的证明或反驳。这以各种方式应用于搜索终止和不终止的证据。 Matchbox 是第一个为一些困难的字符串重写系统提供自动终止证明的程序。
The program Matchbox implements the exact computation of the set of descendants of a regular language, and of the set of non-terminating strings, with respect to an (inverse) match-bounded string rewriting system. Matchbox can search for proof or disproof of a Boolean combination of match-height properties of a given rewrite system, and some of its transformed variants. This is applied in various ways to search for proofs of termination and non-termination. Matchbox is the first program that delivers automated proofs of termination for some difficult string rewriting systems.