Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and

Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and

Cover-Set Inductions

Su Feng

【期刊名称】《计算机科学技术学报（英文版）》 【年(卷),期】2005(020)004

【摘要】The paper presents three formal proving methods for generalized weakly ground terminating property, i.e.,weakly terminating property in a restricted domain of a term rewriting system, one with structural induction, one with cover-set induction, and the third without induction, and describes their mechanization based on a meta-computation model for term rewriting systems-dynamic term rewriting calculus. The methods can be applied to non-terminating, nonconfluent and/or non-left-linear term rewriting systems. They can do \proving\by applying propositions in the proof, as well as \proving\ 【总页数】18页(496-513)

【关键词】automated formal proving;cover-set induction;dynamic term rewriting calculus;term rewriting system;weakly ground termination 【作者】Su Feng

【作者单位】Department of Computer Science, Beijing Normal University, Beijing 100875, P.R. China