Basic Syntactic Mutation

摘要

We give a set of inference rules for E-unification, similar to the inference rules for Syntactic Mutation. If the E is finitely saturated by paramodulation, then we can block certain terms from further inferences. Therefore, E-unification is decidable in NP, as is also the case for Basic Narrowing. However, if we further restrict E, then our algorithm runs in quadratic time, whereas Basic Narrowing does not become polynomial, since it is still nondeterministic.