Improvement of Semantic Labeling Method by KBO for Automated Termination Proof Print

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.