Research on automated confluence proving for term rewriting systems

点击翻译按钮获取中文摘要

The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. Although many automated termination provers of term rewriting systems have been proposed recently, little work is reported on automated confluence provers. This research aims to develop an automated confluence prover ACP for term rewriting systems based on several methods. Concrete results include a reduction-preserving completion method for proving confluence, one side decreasing diagram method for proving commutativity, a path ordering for guaranteeing polynomial size normal forms, a confluence proof method based on persistency. In the first confluence competition for term rewriting systems (IWC 2012), ACP developed by our group has won first place among the three participants.