Basic syntactic mutation

Abstract

We give a set of inference rules for E-unification, similar to the inference rules for Syntactic Mutation. If the E is finitelysaturated 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. © Springer-Verlag Berlin Heidelberg 2002.