@article{oai:kyutech.repo.nii.ac.jp:00000130,
 author = {Hirata, Kouichi and 平田, 耕一 and Yamada, Keizo and Harao, Masateru},
 issue = {5},
 journal = {Journal of Symbolic Computation},
 month = {May},
 note = {The second-order matching problem is to determine whether or not afirst-order term without variables is an instance of a second-order termthat is allowed to contain not only individual variables but also functionvariables. It is well-known that the second-order matching problemis NP-complete in general. In this paper, we first introduce the severalrestrictions for the second-order matching problems, such as the boundednumber, arity and occurrence of function variables, ground that containsno individual variables, flat that contains no function constants, and predicatethat no function variable occurs in the terms of arguments of eachfunction variable. By combining the above restrictions, we give the sharpseparations of tractable second-order matching problems from intractableones. Finally, we compare them with the separations of decidable secondorderunification problems from undecidable ones.},
 pages = {611--628},
 title = {Tractable and intractable second-order matching problems},
 volume = {37},
 year = {2004},
 yomi = {ヒラタ, コウイチ}
}