Volume 1, Number 2 (3-2013)                   SCJ 2013, 1(2): 14-25 | Back to browse issues page

XML Persian Abstract Print

Download citation:
BibTeX | RIS | EndNote | Medlars | ProCite | Reference Manager | RefWorks
Send citation to:

Kadkhoda M, Jalili S, Izadi M. Improvement of Semantic Labeling Method by KBO for Automated Termination Proof . SCJ. 2013; 1 (2) :14-25
URL: http://scj.kashanu.ac.ir/article-1-72-en.html

Abstract:   (3502 Views)

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.

Full-Text [PDF 805 kb]   (1311 Downloads)    
Type of Study: Research | Subject: Special
Received: 2013/08/11 | Accepted: 2013/08/14 | Published: 2013/08/12

Add your comments about this article : Your username or email:
Write the security code in the box

© 2015 All Rights Reserved | Soft Computing Journal

Designed & Developed by : Yektaweb