Boudet, Alexandre Unification of higher-order patterns modulo simple syntactic equational theories. (English) Zbl 0940.03017 Discrete Math. Theor. Comput. Sci. 4, No. 1, 11-30 (2000). Summary: We present an algorithm for unification of higher-order patterns modulo simple syntactic equational theories as defined by C. Kirchner. The algorithm by D. Miller for pattern unification, refined by T. Nipkow is first modified in order to behave as a first-order unification algorithm. Then the mutation rule for syntactic theories of C. Kirchner is adapted to pattern \(E\)-unification. If the syntactic algorithm for a theory \(E\) terminates in the first-order case, then our algorithm will also terminate for pattern \(E\)-unification. The result is a DAG-solved form plus some equations of the form \(\lambda x.F(x) = \lambda x. F(x^{\pi})\) where \(x^{\pi}\) is a permutation of \(x\). When all function symbols are decomposable these latter equations can be discarded, otherwise the compatibility of such equations with the solved form remains open. MSC: 03B35 Mechanization of proofs and logical operations 68Q42 Grammars and rewriting systems Keywords:unification of higher-order patterns; syntactic equational theories PDFBibTeX XMLCite \textit{A. Boudet}, Discrete Math. Theor. Comput. Sci. 4, No. 1, 11--30 (2000; Zbl 0940.03017) Full Text: EuDML EMIS