%0 Journal Article
%T Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions
%A Su Feng
%A <br>Su
%A Feng
%J 计算机科学技术学报
%D 2005
%I 
%X 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, non-confluent 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.
%K automated formal proving
%K cover-set induction
%K dynamic term rewriting calculus
%K term rewriting system
%K weakly ground termination<br>内存驱留程序
%K 文件系统
%K TRS
%K 计算机
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=F57FEF5FAEE544283F43708D560ABF1B&aid=76E1AB13693367D8C696B4F783C1FA8C&yid=2DD7160C83D0ACED&vid=A04140E723CB732E&iid=E158A972A605785F&sid=C4490A71BEB872FA&eid=F9A6B6F259CE5121&journal_id=1000-9000&journal_name=计算机科学技术学报&referenced_num=0&reference_num=15