Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions
冯速 · Acta Scientiarum Naturalium Universitatis Sunyatseni · 2005
The paper presents three formal 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 forward proving by applying propositions in the proof, as well as backward proving by discovering lemmas during the proof.