Tractable and Intractable Second-Order Matching Problems

Abstract

The second-order matching problem is the problem of determining, for a finite set $\left\{ {\left\langle {t_i s_i } \right\rangle \left| {i \in I} \right.} \right\}$ of pairs of a second-order term t _i and a first-order closed term s _i , called a matching expression, whether or not there exists a substitution σ such that t ⁱσ = s ⁱ for each i ∈ I. It is well-known that the second-order matching problem is NP-complete. In this paper, we introduce the following restrictions of a matching expression: k-ary, k-fv , predicate, ground, and function-free. Then, we show that the second-order matching problem is NP-complete for a unary predicate, a unary ground, a ternary function-free predicate, a binary function-free ground, and an 1-fv predicate matching expressions, while it is solvable in polynomial time for a binary function-free predicate, a unary function-free, a k-fv function-free (k ≥ 0), and a ground predicate matching expressions.

This work is partially supported by the Japanese Ministry of Education, Grant-in-Aid for Exploratory Research 10878055 and Kayamori Foundation of Informational Science Advancement.