Automated confluence proof by decreasing diagrams based on rule-labelling

Takahito Aoto

研究成果: Conference contribution

13 被引用数 (Scopus)

抄録

Decreasing diagrams technique (van Oostrom, 1994) is a technique that can be widely applied to prove confluence of rewrite systems. To directly apply the decreasing diagrams technique to prove confluence of rewrite systems, rule-labelling heuristic has been proposed by van Oostrom (2008). We show how constraints for ensuring confluence of term rewriting systems constructed based on the rule-labelling heuristic are encoded as linear arithmetic constraints suitable for solving the satisfiability of them by external SMT solvers. We point out an additional constraint omitted in (van Oostrom, 2008) that is needed to guarantee the soundness of confluence proofs based on the rule-labelling heuristic extended to deal with non-right-linear rules. We also present several extensions of the rule-labelling heuristic by which the applicability of the technique is enlarged.

本文言語English
ホスト出版物のタイトルProceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010
ページ7-16
ページ数10
出版ステータスPublished - 2010
イベント21st International Conference on Rewriting Techniques and Applications, RTA 2010 - Edinburgh, United Kingdom
継続期間: 2010 7 112010 7 13

出版物シリーズ

名前Leibniz International Proceedings in Informatics, LIPIcs
6
ISSN(印刷版)1868-8969

Other

Other21st International Conference on Rewriting Techniques and Applications, RTA 2010
国/地域United Kingdom
CityEdinburgh
Period10/7/1110/7/13

ASJC Scopus subject areas

  • ソフトウェア

フィンガープリント

「Automated confluence proof by decreasing diagrams based on rule-labelling」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル