Date Added: Dec 2009
Term rewrite systems have been extensively used in order to model computer programs for the purpose of formal verification. This is in particular true if the termination behavior of computer programs is investigated, and automatic termination proving for term rewrite systems has received increased interest in recent years. Ordinary term rewrite systems, however, exhibit serious drawbacks. First, they do not provide a tight integration of natural numbers or integers. Since the pre-defined semantics of these primitive data types cannot be utilized, reasoning about termination of ordinary term rewrite systems operating on numbers is often cumbersome or even impossible. Second, ordinary term rewrite system cannot accurately model collection data structures such as sets or multisets which are supported by many high-level programming languages such as Maude or OCaml.