A New Order Which Proved the Termination of Term Rewriting System
Chen Chen, Wei-Hong Chen · 2009
Term rewriting is a branch of theoretical computer science which combines elements of logic, universal algebra, automated theorem proving and functional programming, it has lots of application in math and computer field. Termination is a very important property of term rewriting system, and the standard detected measure is constructing a reduction order, but a right order is difficult to construct. A new reduction order which called vector order is given, it has obvious advantage in realization and complexity compared with some mostly existent reduction order which as polynomial order and lexicographic path order.