The Algorithm And Implementation Of Automatic E-unifier Generator

In the field of automated deduction, natural language understanding, theorem proving and rewriting theory, unification theory is a very fundamental process. Nowadays researchers have designed several efficient unification algorithms and many automated tools have also been developed. However, there is no efficient practice of an E-unifier generator. In this paper, we propose an efficient method to construct an E-unifier generator. We begin from the most intuitive recursion method an then in order to avoid repeated access to a node, the new algorithm brings in a new data-directed acyclic graph, we also use the directed edge in the graph to represent substitutions. In this way, we can get an almost linear algorithm under ordinary circumstances. But this algorithm can still be improved. The solution lies in the reduction from the problem of combination of equational classes to the unification of terms and at the same time, we can use the combining by rank and the path compressing strategies during the process of sets combination. As a result, our algorithm can get closer to a linear one. Afterwards, we begin to expand the problems of syntactic unification to E-Unification and seek solutions to the problems in E-Unification. Our main idea in this paper is to generate corresponding sets of terms according to the mapping from terms to shapes of trees. The set is in accordance with the original term and the properties of the E-Unification problem. In this way, we can apply our existing syntactic unification solution to the E-Unification problem. This proposal is able to solve E-unification problems in which case the Diophantine Equations is unable to help. Hence, the method is practical enough for other research works. In the field of Model-Checking, the core of the current security model checker is based on the syntactic unification. These checkers use the Dolev-Yao Model to model for the ability of the attackers. But if the attackers have the ability of calculation, their attack level will exceed that the Dolev-Yao Model has described. The solution to this is to extend the syntactic unification to the equational unification. So in this paper, we introduce something background about model-checking and security protocol verification.