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.
Kadkhoda, M., Jalili, S., & Izadi, M. (2021). Improvement of Semantic Labeling Method by KBO for Automated Termination Proof. Soft Computing Journal, 1(2), 14-25.
MLA
Mohammad Kadkhoda; Saeed Jalili; Mohammad Izadi. "Improvement of Semantic Labeling Method by KBO for Automated Termination Proof", Soft Computing Journal, 1, 2, 2021, 14-25.
HARVARD
Kadkhoda, M., Jalili, S., Izadi, M. (2021). 'Improvement of Semantic Labeling Method by KBO for Automated Termination Proof', Soft Computing Journal, 1(2), pp. 14-25.
VANCOUVER
Kadkhoda, M., Jalili, S., Izadi, M. Improvement of Semantic Labeling Method by KBO for Automated Termination Proof. Soft Computing Journal, 2021; 1(2): 14-25.
)
