We have developed an expert system, called TERMINATOR, whichproves the termination of computer programs written as a set of rewriterules. In TERMINATOR, the knowledge of the proof techniques isrepresented by a class of partial orderings called path orderings. Inparticular, the system incorporates the new and powerful orderingscalled RPOES and KNSES, which are presented in this paper. The twoorderings generalize the well-known RPO and KNS orderings with an ideaof the extended status proposed in this paper, and can be successfullyused to prove the termination of rewrite rules that can not be proved bythe conventional knowledge
展开▼
