• DocumentCode
    2180203
  • Title

    Orderings for term-rewriting systems

  • Author

    Dershowitz, Nachum

  • fYear
    1979
  • fDate
    29-31 Oct. 1979
  • Firstpage
    123
  • Lastpage
    131
  • Abstract
    Methods of proving that a term-rewriting system terminates are presented. They are based on the notion of "simplification orderings", orderings in which any term that is homeomorphically embeddable in another is smaller than the other. A particularly useful class of simplification orderings, the "recursive path orderings", is defined. Several examples of the use of such orderings in termination proofs are given.
  • Keywords
    Computer science;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Foundations of Computer Science, 1979., 20th Annual Symposium on
  • Conference_Location
    San Juan, Puerto Rico
  • ISSN
    0272-5428
  • Type

    conf

  • DOI
    10.1109/SFCS.1979.32
  • Filename
    4568008