Linear Higher-Order Matching Is NP-Complete

1. Angluin, D.: Finding patterns common to a set of strings. Journal of Computer and System Sciences 21, 46–62 (1980)

   Article  MATH  MathSciNet  Google Scholar 

2. Cervesato, I., Pfenning, F.: Linear higher-order pre-unification. In: Proceedings of the 12th annual IEEE symposium on logic in computer science, pp. 422–433 (1997)

   Google Scholar 

3. Comon, H.: Completion of rewrite systems with membership constraints. Part I: Deduction rules. Journal of Symbolic Computation 25(4), 397–419 (1998)

   Article  MATH  MathSciNet  Google Scholar 

4. Comon, H.: Completion of rewrite systems with membership constraints. Part II: Constraint solving. Journal of Symbolic Computation 25(4), 421–453 (1998)

   Article  MATH  MathSciNet  Google Scholar 

5. Dowek, G.: Third order matching is decidable. Annals of Pure and Applied Logic 69(2-3), 135–155 (1994)

   Article  MATH  MathSciNet  Google Scholar 

6. Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)

   Article  MATH  MathSciNet  Google Scholar 

7. Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoretical Computer Science 13(2), 225–230 (1981)

   Article  MATH  MathSciNet  Google Scholar 

8. Huet, G.: The undecidability of unification in third order logic. Information and Control 22(3), 257–267 (1973)

   Article  MATH  MathSciNet  Google Scholar 

9. Huet, G.: A unification algorithm for typed λ-calculus. Theoretical Computer Science 1, 27–57 (1975)

   Article  MathSciNet  Google Scholar 

10. Huet, G.: Résolution d’équations dans les langages d’ordre 1, 2,..., w. Thèse de Doctorat d’Etat, Université Paris 7 (1976)

    Google Scholar 

11. Levy, J.: Linear second-order unification. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 332–346. Springer, Heidelberg (1996)

    Google Scholar 

12. Levy, J.: Decidable and undecidable second-order unification problems. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 47–60. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

13. Merenciano, J.M., Morrill, G.: Generation as deduction on labelled proof nets. In: Retoré, C. (ed.) LACL 1996. LNCS (LNAI), vol. 1328, pp. 310–328. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

14. Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation 1(4), 497–536 (1991)

    Article  MATH  MathSciNet  Google Scholar 

15. Moortgat, M.: Categorial type logic. In: van Benthem, J., ter Meulen, A. (eds.) Handbook of Logic and Language. ch. 2, Elsevier, Amsterdam (1997)

    Google Scholar 

16. Morrill, G.: Type Logical Grammar: Categorial Logic of Signs. Kluwer Academic Publishers, Dordrecht (1994)

    MATH  Google Scholar 

17. Padovani, V.: Filtrage d’ordre supérieure. Thèse de Doctorat, Université de Paris 7 (1996)

    Google Scholar 

18. Paulson, L.C.: Isabelle, a generic theorem prover. LNCS, vol. 828. Springer, Heidelberg (1994)

    MATH  Google Scholar 

19. Schmidt-Schauss, M., Schulz, K.U.: Solvability of context equations with two context variables is decidable. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 67–81. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

20. Snyder, W., Gallier, J.: Higher order unification revisited: Complete sets of transformations. Journal of Symbolic Computation 8(1-2), 101–140 (1989)

    Article  MATH  MathSciNet  Google Scholar 

21. Wierzbicki, T.: Complexity of the higher order matching. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 82–96. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

Download references