دانشگاه کاشان محاسبات نرم 2322-3707 1 2 2021 05 23 Improvement of Semantic Labeling Method by KBO for Automated Termination Proof توسعه روش SL با ترتیب KBO برای اثبات خودکار پایان‌پذیری سیستم بازنویسی ترم - مقاله برگزیده هفدهمین کنفرانس ملی انجمن کامپیوتر ایران 14 25 111359 FA محمد کدخدا سعید جلیلی دانشگاه تربیت مدرس محمد ایزدی دانشگاه صنعتی شریف Journal Article 2021 05 23  The term rewriting systems (TRSs) is an abstract model of functional languages. The termination proving of TRSs is necessary for confirming accuracy of functional languages. The semantic labeling (SL) is a complete method for proving termination. The semantic part of SL is given by a quasi-model of the rewrite rules. The most power of SL is related to infinite models that is difficult for support by tools of automated termination proving. In this paper, we combined the SL method with natural numbers and Knuth-Bendix order (KBO) so that one can automatically prove termination using infinite models. We: (1) made a generalization based on KBO, called labeling Knuth-Bendix order (ℓKBO), (2) showed its ability in proving termination of TRSs, (3) we introduced an algorithm to automatically search a ℓKBO for a given TRS and (4) successfully tested the algorithm functionality on TPDB 3.1, a data set of TRSs.  سی ترم   https://scj.kashanu.ac.ir/article_111359_bdbeb6d88d15fefb533a97c35810810e.pdf