Modular AC Unification of Higher-Order Patterns

摘要: This paper considers AC unification of higher-order patterns (short: patterns), which are simply typed λ-terms in long β-normal form where the arguments a free variable always η-equal to distinct bound variables. A pattern is called pure if it can be written as λx1 ... λxk.s1+...+sn, + an function symbol and each si either or subterm starting with variable. As main part paper, we propose algorithm for patterns, parameterized by first-order AC1 algorithm. The terminating complete whenever parameterizing is. all obtained combining patterns. Theoretically, result presented here implies decidability Practically, our used extend logic programming proof systems operators.