基于项重写的形式化排序方法及应用

摘要

The vector order which based on term rewriting was constructed, it was closed under substitution and composition, and had advantage in realization, the number of transferring rules and automatization compared with the other ordering methods. An application in information security was given, i.e. an arithmetic which resolved the problem of XOR equivalent unification, it analysed all conditions and returns the solution.%构建一个基于项重写理论的向量序,该序具有替换、组合封闭等性质,在可实现性、规则调用次数和自动化实现等方面优于目前主要应用的几个形式化排序方法;并给出向量序在信息安全领域中的应用,即解决异或操作等价合一问题的实现算法,该算法分析合一的所有条件,并在合一成功时输出合一解.