Generating polynomial orderings for termination proofs
| Author(s) : | Jurgen Giesl, |
| Publisher : | N/A |
| Publication Date : | 1995 |
| ISSN : | N/A |
| Abstract : | Abstract. Most systems for the automation of termination proofs using polynomial orderings are only semi-automatic, i.e. the "right " polynomial ordering has to be given by the user. We show that a variation of Lankford 's partial derivative technique leads to an easier and slightly more powerful method than most other semi-automatic approaches. Based on this technique we develop a method for the automated synthesis of a suited polynomial ordering. 1, |