{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:26Z","timestamp":1725484286709},"publisher-location":"Berlin, Heidelberg","reference-count":117,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_2","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T20:47:53Z","timestamp":1179607673000},"page":"3-12","source":"Crossref","is-referenced-by-count":9,"title":["Higher Order Unification 30 Years Later"],"prefix":"10.1007","author":[{"given":"G\u00e9rard","family":"Huet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01621471","volume":"30","author":"G. Amiot","year":"1990","unstructured":"G. Amiot. The undecidability of the second order predicate unification problem. Archive for mathematical logic, 30:193\u2013199, 1990.","journal-title":"Archive for mathematical logic"},{"key":"2_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BFb0012823","volume-title":"Proceedings of the 9th Int. Conference on Automated Deduction (CADE-9)","author":"D. M. A. Felty","year":"1988","unstructured":"Dale Miller Amy Felty. Specifying theorem provers in a higher-order logic programming language. In Proceedings of the 9th Int. Conference on Automated Deduction (CADE-9), volume 310 of Lecture Notes in Computer Science, pages 61\u201380. Springer-Verlag, Argonne, Illinois, 1988."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Penny Anderson. Represnting proof transformations for program optimization. In Proceedings of the 12th Int. Conference on Automated Deduction (CADE-12), volume 814 of Lecture Notes in Artificial Intelligence, pages 575\u2013589, Nancy, France, 1994. Springer-Verlag.","DOI":"10.1007\/3-540-58156-1_42"},{"issue":"3","key":"2_CR4","doi-asserted-by":"publisher","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P.B. Andrews","year":"1971","unstructured":"P.B. Andrews. Resolution in type theory. The Journal of Symbolic Logic, 36(3):414\u2013432, 1971.","journal-title":"The Journal of Symbolic Logic"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P.B. Andrews","year":"1996","unstructured":"P.B. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning, and H. Xi. Tps: a theorem proving system for classical type theory. J. of Automated Reasoning, 16:321\u2013353, 1996.","journal-title":"J. of Automated Reasoning"},{"key":"2_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BFb0016859","volume-title":"International Conference on Constaints in Computational Logic","author":"J. Avenhaus","year":"1994","unstructured":"J. Avenhaus and C.A. Lor\u00eda-S\u00e1enz. Higher-order conditional rewriting and narrowing. In J.-P. Jouannaud, editor, International Conference on Constaints in Computational Logic, volume 845 of Lecture Notes in Computer Science, pages 269\u2013284. Springer-Verlag, 1994."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Yves Bekkers, Olivier Ridoux, and Lucien Ungaro. Dynamic memory management for sequential logic programming languages. In IWMM, pages 82\u2013102, 1992.","DOI":"10.1007\/BFb0017184"},{"key":"2_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1007\/BFb0054248","volume-title":"Proceedings of the 15th Int. Conference on Automated Deduction (CADE-15)","author":"C. Benzm\u00fcller","year":"1998","unstructured":"C. Benzm\u00fcller. Extensional higher-order resolution. In Proceedings of the 15th Int. Conference on Automated Deduction (CADE-15), volume 1421 of Lecture Notes in Artificial Intelligence, pages 56\u201371. Springer-Verlag, Lindau, Germany, 1998."},{"key":"2_CR9","volume-title":"Doctoral Dissertation","author":"C. Benzm\u00fcller","year":"1999","unstructured":"C. Benzm\u00fcller. Equality and extensionality in automated higher-order theorem proving. Doctoral Dissertation, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, 1999."},{"key":"2_CR10","unstructured":"Fr\u00e9d\u00e9ric Blanqui. Th\u00e9orie des types et r\u00e9\u00e9criture. Th\u00e8se de Doctorat, Universit\u00e9 Paris-Sud, 2001."},{"key":"2_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-60609-2_18","volume-title":"SOFSEM: Theory and Practice of Informatics","author":"P. Borovansk\u00fd","year":"1995","unstructured":"P. Borovansk\u00fd. Implementation of higher-order unification based on calculus of explicit substitution. In M. Barto\u0161ek, J. Staudek, and J. Wiedermann, editors, SOFSEM: Theory and Practice of Informatics, volume 1012 in Lecture Notes in Computer Science, pages 363\u2013368. Springer-Verlag, 1995."},{"key":"2_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/BFb0017445","volume-title":"Principles and Practice of Constraint Programming","author":"A. Boudet","year":"1997","unstructured":"A. Boudet and E. Contejean. AC-unification of higher-order patterns. In G. Smolka, editor, Principles and Practice of Constraint Programming, volume 1330 of Lecture Notes in Computer Science, pages 267\u2013281. Springer-Verlag, 1997."},{"key":"2_CR13","unstructured":"D. Briaud. Higher order unification as typed narrowing. Technical Report 96-R-112, Centre de recherche en informatique de Nancy, 1996."},{"key":"2_CR14","unstructured":"Pascal Brisset and Olivier Ridoux. The architecture of an implementation of lambdaprolog: Prolog\/mali. Technical Report RR-2392, INRIA, Oct. 1994."},{"key":"2_CR15","first-page":"313","volume":"9","author":"M. Kohlhase","year":"2001","unstructured":"M. Kohlhase, C. Gardent, and K. Konrad. Higher-order colored unification: A linguistic application. J. of Logic, Language and Information, 9:313\u2013338, 2001.","journal-title":"J. of Logic, Language and Information"},{"issue":"1","key":"2_CR16","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(1):56\u201368, 1940.","journal-title":"The Journal of Symbolic Logic"},{"key":"2_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/BFb0028013","volume-title":"Conference on Computer Science Logic","author":"H. Comon","year":"1997","unstructured":"H. Comon and Y. Jurski. Higher-order matching and tree automata. In M. Nielsen and W. Thomas, editors, Conference on Computer Science Logic, volume 1414 of Lecture Notes in Computer Science, pages 157\u2013176. Springer-Verlag, 1997."},{"key":"2_CR18","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0304-3975(93)90075-5","volume":"114","author":"D.J. Dougherty","year":"1993","unstructured":"D.J. Dougherty. Higher-order unification via combinators. Theoretical Computer Science, 114:273\u2013298, 1993.","journal-title":"Theoretical Computer Science"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"D.J. Dougherty and P. Johann. A combinatory logic approach to higher-order E-unification. In D. Kapur, editor, Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 79\u201393. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_157"},{"key":"2_CR20","unstructured":"G. Dowek. D\u00e9monstration automatique dans le calcul des constructions. Th\u00e8se de Doctorat, Universit\u00e9 de Paris VII, 1991."},{"issue":"12","key":"2_CR21","first-page":"951","volume":"312","author":"G. Dowek","year":"1991","unstructured":"G. Dowek. L\u2019ind\u00e9cidabilit\u00e9 du filtrage du troisi\u00e8me ordre dans les calculs avec types d\u00e9pendants ou constructeurs de types (the undecidability of third order pattern matching in calculi with dependent types or type constructors). Comptes Rendus \u00e0 l\u2019Acad\u00e9mie des Sciences, I, 312(12):951\u2013956, 1991. Erratum, ibid. I, 318, 1994, p. 873.","journal-title":"Comptes Rendus \u00e0 l\u2019Acad\u00e9mie des Sciences"},{"key":"2_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/3-540-54345-7_58","volume-title":"Mathematical Foundation of Computer Science","author":"G. Dowek","year":"1991","unstructured":"G. Dowek. A second-order pattern matching algorithm in the cube of typed \u03bb-calculi. In A. Tarlecki, editor, Mathematical Foundation of Computer Science, volume 520 of Lecture notes in computer science, pages 151\u2013160. Springer-Verlag, 1991."},{"issue":"3","key":"2_CR23","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1093\/logcom\/3.3.287","volume":"3","author":"G. Dowek","year":"1993","unstructured":"G. Dowek. A complete proof synthesis method for the cube of type systems. Journal of Logic and Computation, 3(3):287\u2013315, 1993.","journal-title":"Journal of Logic and Computation"},{"key":"2_CR24","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1016\/0304-3975(93)90175-S","volume":"107","author":"G. Dowek","year":"1993","unstructured":"G. Dowek. The undecidability of pattern matching in calculi where primitive recursive functions are representable. Theoretical Computer Science, 107:349\u2013356, 1993.","journal-title":"Theoretical Computer Science"},{"key":"2_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BFb0037103","volume-title":"Typed Lambda Calculi and Applications","author":"G. Dowek","year":"1993","unstructured":"G. Dowek. The undecidability of typability in the lambda-pi-calculus. In M. Bezem and J.F. Groote, editors, Typed Lambda Calculi and Applications, volume 664 in Lecture Notes in Computer Science, pages 139\u2013145. Springer-Verlag, 1993."},{"key":"2_CR26","unstructured":"G. Dowek. A unification algorithm for second-order linear terms. Manuscript, 1993."},{"key":"2_CR27","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0168-0072(94)90083-3","volume":"69","author":"G. Dowek","year":"1994","unstructured":"G. Dowek. Third order matching is decidable. Annals of Pure and Applied Logic, 69:135\u2013155, 1994.","journal-title":"Annals of Pure and Applied Logic"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"G. Dowek. Higher-Order Unification and Matching, chapter 16, pages 1009\u20131062. Elsevier, 2001.","DOI":"10.1016\/B978-044450813-3\/50018-7"},{"key":"2_CR29","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1006\/inco.1999.2837","volume":"157","author":"G. Dowek","year":"2000","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions. Information and Computation, 157:183\u2013235, 2000.","journal-title":"Information and Computation"},{"key":"2_CR30","unstructured":"G. Dowek, T. Hardin, C. Kirchner, and F. Pfenning. Unification via explicit substitutions: the case of higher-order patterns. In M. Maher, editor, Joint International Conference and Symposium on Logic Programming, pages 259\u2013273. The MIT Press, 1996."},{"key":"2_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/3-540-51081-8_104","volume-title":"Internatinal Conference on Rewriting Techniques and Applications","author":"C.M. Elliott","year":"1989","unstructured":"C.M. Elliott. Higher-order unification with dependent function types. In N. Dershowitz, editor, Internatinal Conference on Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, pages 121\u2013136. Springer-Verlag, 1989."},{"key":"2_CR32","unstructured":"C.M. Elliott. Extensions and applications of higher-order unification. PhD thesis, Carnegie Mellon University, 1990."},{"key":"2_CR33","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0168-0072(88)90015-2","volume":"39","author":"W.M. Farmer","year":"1988","unstructured":"W.M. Farmer. A unification algorithm for second-order monadic terms. Annals of Pure and applied Logic, 39:131\u2013174, 1988.","journal-title":"Annals of Pure and applied Logic"},{"key":"2_CR34","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0304-3975(06)80003-4","volume":"87","author":"W.M. Farmer","year":"1991","unstructured":"W.M. Farmer. Simple second order languages for which unification is undecidable. Theoretical Computer Science, 87:25\u201341, 1991.","journal-title":"Theoretical Computer Science"},{"key":"2_CR35","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/BF00881900","volume":"11","author":"A. Felty","year":"1993","unstructured":"Amy Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11:43\u201381, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR36","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1023\/A:1008330623446","volume":"9","author":"C. Gardent","year":"2000","unstructured":"C. Gardent. Deaccenting and higher-order unification. J. of Logic, Language and Information, 9:313\u2013338, 2000.","journal-title":"J. of Logic, Language and Information"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"C. Gardent and M. Kohlhase. Focus and higher-order unification. In 16th International Conference on Computational Linguistics, Copenhagen, 1996.","DOI":"10.3115\/992628.992703"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"C. Gardent and M. Kohlhase. Higher-order coloured unification and natural language semantics. In ACL, editor, 34th Annual Meeting of the Association for Computational Linguistics, Santa Cruz, 1996.","DOI":"10.3115\/981863.981864"},{"key":"2_CR39","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W.D. Goldfarb","year":"1981","unstructured":"W.D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225\u2013230, 1981.","journal-title":"Theoretical Computer Science"},{"key":"2_CR40","doi-asserted-by":"crossref","unstructured":"J. Goubault. Higher-order rigid E-unification. In F. Pfenning, editor, 5th International Conference on Logic Programming and Automated Reasoning, volume 822 in Lecture Notes in Artificial Intelligence, pages 129\u2013143. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58216-9_34"},{"key":"2_CR41","unstructured":"W.E. Gould. A matching procedure for \u03c9-order logic. Scientific report 4, AFCRL 66-781 (contract AF 19 (628)-3250) AD 646 560."},{"key":"2_CR42","unstructured":"J.R. Guard. Automated logic for semi-automated mathematics. Scientific report 1, AFCRL 64-411 (contract AF 19 (628)-3250) AS 602 710, 1964."},{"key":"2_CR43","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"588","DOI":"10.1007\/3-540-52885-7_116","volume-title":"Conference on Automated Deduction","author":"M. Hagiya","year":"1990","unstructured":"M. Hagiya. Programming by example and proving by example using higher-order unification. In M.E. Stickel, editor, Conference on Automated Deduction, volume 449 in Lecture Notes in Computer Science, pages 588\u2013602. Springer-Verlag, 1990."},{"key":"2_CR44","unstructured":"M. Hagiya. Higher-order unification as a theorem proving procedure. In K. Furukawa, editor, International Conference on Logic Programming, pages 270\u2013284. MIT Press, 1991."},{"key":"2_CR45","unstructured":"John Hannan and Dale Miller. Uses of higher-order unification for implementing programs transformers. In R.A. Kowalski an K.A. Bowen, editor, International Conference and Symposium on Logic Programming, pages 942\u2013959, 1988."},{"key":"2_CR46","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"G. Huet","year":"1973","unstructured":"G. Huet. The undecidability of unification in third order logic. Information and Control, 22:257\u2013267, 1973.","journal-title":"Information and Control"},{"key":"2_CR47","unstructured":"G. Huet. R\u00e9solution d\u2019\u00e9quations dans les langages d\u2019ordre 1,2,..., \u03c9. Th\u00e8se d\u2019\u00c9tat, Universit\u00e9 de Paris VII, 1976."},{"key":"2_CR48","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"G. Huet and B. Lang. Proving and applying program transformations expressed with second order patterns. Acta Informatica, 11:31\u201355, 1978.","journal-title":"Acta Informatica"},{"key":"2_CR49","unstructured":"G\u00e9rard Huet. Constrained resolution: A complete method for higher order logic. PhD thesis, Case Western University, Aug. 1972."},{"key":"2_CR50","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0304-3975(76)90021-9","volume":"3","author":"D.C. Jensen","year":"1976","unstructured":"D.C. Jensen and T. Pietrzykowski. Mechanizing \u03c9-order type theory through unification. Theoretical Computer Science, 3:123\u2013171, 1976.","journal-title":"Theoretical Computer Science"},{"key":"2_CR51","series-title":"Lect Notes Comput Sci","first-page":"147","volume-title":"Proceedings of the 3rd Int. Conference on Typed Lambda Calculus and Applications (TLCA\u2019 97)","author":"F. Pfenning","year":"1997","unstructured":"Frank Pfenning, Jo\u00eblle Despeyroux, and Carsten Sch\u00fcrmann. Primitive recursion for higher-order syntax. In R. Hindley, editor, Proceedings of the 3rd Int. Conference on Typed Lambda Calculus and Applications (TLCA\u2019 97), volume 1210 of Lecture Notes in Computer Science, pages 147\u2013163, Nancy, France, 1997. Springer-Verlag."},{"key":"2_CR52","doi-asserted-by":"crossref","unstructured":"Patricia Johann and Michael Kohlhase. Unification in an extensional lambda calculus with ordered function sorts and constant overloading. In Alan Bundy, editor, Conference on Automated Deduction, volume 814 in Lecture Notes in Artificial Intelligence, pages 620\u2013634. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_45"},{"key":"2_CR53","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BFb0027003","volume-title":"Algebraic and Logic Programming, International Joint Conference ALP\u201997-HOA\u201997","author":"C. Kirchner","year":"1997","unstructured":"C. Kirchner and Ch. Ringeissen. Higher-order equational unification via explicit substitutions. In M. Hanus, J. Heering, and K. Meinke, editors, Algebraic and Logic Programming, International Joint Conference ALP\u201997-HOA\u201997, volume 1298 of Lecture Notes in Computer Science, pages 61\u201375. Springer-Verlag, 1997."},{"key":"2_CR54","unstructured":"K. Kwon and G. Nadathur. An instruction set for higher-order hereditary harrop formulas (extended abstract). In Proceedings of the Workshop on the lambda Prolog Programming Language, UPenn Technical Report MS-CIS-92-86, 1992."},{"key":"2_CR55","unstructured":"Peter Lee, Frank Pfenning, John Reynolds, Gene Rollins, and Dana Scott. Research on semantically based program-design environments: The ergo project in 1988. Technical Report CMU-CS-88-118, Computer Science Department, Carnegie Mellon University, 1988."},{"key":"2_CR56","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-61464-8_63","volume-title":"Rewriting Techniques and Applications","author":"J. Levy","year":"1996","unstructured":"J. Levy. Linear second order unification. In H. Ganzinger, editor, Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 332\u2013346. Springer-Verlag, 1996."},{"key":"2_CR57","unstructured":"Jordi Levy and Margus Veanes. On unification problems in restricted second-order languages. In Annual Conf. of the European Ass. of Computer Science Logic (CSL98), Brno, Czech Republic, 1998."},{"key":"2_CR58","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/10721975_11","volume-title":"Proceedings of the 11th Int. Conf. on Rewriting Techniques and Applications (RTA 2000)","author":"J. Levy","year":"2000","unstructured":"Jordi Levy and Mateu Villaret. Linear second-order unification and context unification with tree-regular constraints. In Proceedings of the 11th Int. Conf. on Rewriting Techniques and Applications (RTA 2000), volume 1833 of Lecture Notes in Computer Science, pages 156\u2013171, Norwich, UK, 2000. Springer-Verlag."},{"key":"2_CR59","unstructured":"R. Loader. The undecidability of \u03bb-definability. To appear in Church memorial volume, 1994."},{"key":"2_CR60","unstructured":"R. Loader. Higher order \u03b2 matching is undecidable. Private communication, 2001."},{"key":"2_CR61","unstructured":"C.L. Lucchesi. The undecidability of the unification problem for third order languages. Technical Report CSRR 2060, Department of applied analysis and computer science, University of Waterloo, 1972."},{"key":"2_CR62","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/BF00630923","volume":"14","author":"S. M. Shieber","year":"1991","unstructured":"Stuart M. Shieber Mary Dalrymple and Fernando C.N. Pereira. Ellipsis and higher-order unification. Linguistic and Philosophy, 14:399\u2013452, 1991.","journal-title":"Linguistic and Philosophy"},{"key":"2_CR63","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R. Mayr","year":"1998","unstructured":"R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192:3\u201329, 1998.","journal-title":"Theoretical Computer Science"},{"key":"2_CR64","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/504077.504080","volume":"3","author":"R. McDowell","year":"2002","unstructured":"Raymond McDowell and Dale Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic (TOCL), 3:80\u2013136, 2002.","journal-title":"ACM Transactions on Computational Logic (TOCL)"},{"key":"2_CR65","unstructured":"Dale Miller. Abstractions in logic programming. In P. Odifreddi, editor, Logic and computer science, pages 329\u2013359. Academic Press, 1991."},{"key":"2_CR66","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D. Miller","year":"1992","unstructured":"Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14:321\u2013358, 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"2_CR67","unstructured":"Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In IEEE Symposium on Logic Programming, pages 247\u2013255, San Francisco, California, 1986."},{"key":"2_CR68","doi-asserted-by":"crossref","unstructured":"Dale Miller and Gopalan Nadathur. Some uses of higher-order logic in computational linguistics. In 24th Annual Meeting of the Association for Computational Linguistics, pages 247\u2013255, 1986.","DOI":"10.3115\/981131.981165"},{"key":"2_CR69","doi-asserted-by":"crossref","unstructured":"O. M\u00fcller and F. Weber. Theory and practice of minimal modular higher-order E-unification. In A. Bundy, editor, Conference on Automated Deduction, volume 814 in Lecture Notes in Artificial Intelligence, pages 650\u2013664. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_47"},{"key":"2_CR70","unstructured":"Gopalan Nadathur. An explicit substitution notation in a \u03bbprolog implementation. In First International Workshop on Explicit Substitutions, 1998."},{"key":"2_CR71","unstructured":"Gopalan Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, Dec. 1986."},{"key":"2_CR72","doi-asserted-by":"crossref","first-page":"777","DOI":"10.1145\/96559.96570","volume":"37","author":"G. Nadathur","year":"1990","unstructured":"Gopalan Nadathur and Dale Miller. Higher-order horn clauses. J. of the Association for Computing Machinery, 37:777\u2013814, 1990.","journal-title":"J. of the Association for Computing Machinery"},{"key":"2_CR73","doi-asserted-by":"crossref","unstructured":"Gopalan Nadathur and Dale Miller. Higher-order logic programming. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of logic in artificial intelligence and logic programming, volume 5, pages 499\u2013590. Clarendon Press, 1998.","DOI":"10.1093\/oso\/9780198537922.003.0011"},{"key":"2_CR74","doi-asserted-by":"crossref","unstructured":"Gopalan Nadathur and D.J. Mitchell. System description: A compiler and abstract machine based implementation of \u03bbprolog. In Conference on Automated Deduction, 1999.","DOI":"10.1007\/3-540-48660-7_25"},{"key":"2_CR75","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order critical pairs. In Logic in Computer Science, pages 342\u2013349, 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"2_CR76","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/3-540-59200-8_61","volume-title":"Proceedings of the 6th Int. Conf. on Rewriting Techniques and Applications (RTA-95)","author":"T. Nipkow","year":"1995","unstructured":"T. Nipkow. Higher-order rewrite systems. In Proceedings of the 6th Int. Conf. on Rewriting Techniques and Applications (RTA-95), volume 914 of Lecture Notes in Computer Science, pages 256\u2013256, Keiserlautern, Germany, 1995. Springer-Verlag."},{"key":"2_CR77","unstructured":"T. Nipkow and Ch. Prehofer. Higher-order rewriting and equational reasoning. In W. Bibel and P.H. Schmitt, editors, Automated Deduction-A Basis for Applications, volume 1, pages 399\u2013430. Kluwer, 1998."},{"key":"2_CR78","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-53904-2_97","volume-title":"Proceedings of the 4th Int. Conf. on Rewriting Techniques and Applications (RTA)","author":"T. Nipkow","year":"1991","unstructured":"Tobias Nipkow and Zhenyu Qian. Modular higher-order e-unification. In Proceedings of the 4th Int. Conf. on Rewriting Techniques and Applications (RTA), volume 488 of Lecture Notes in Computer Science, pages 200\u2013214. Springer-Verlag, 1991."},{"key":"2_CR79","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/BF00885767","volume":"12","author":"T. Nipkow","year":"1994","unstructured":"Tobias Nipkow and Zhenyu Qian. Reduction and unification in lambda calculi with a general notion of subtype. Journal of Automated Reasoning, 12:389\u2013406, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR80","unstructured":"V. Padovani. Fourth-order matching is decidable. Manuscript, 1994."},{"key":"2_CR81","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/3-540-61780-9_71","volume-title":"Types for Proof and Programs 1995","author":"V. Padovani","year":"1996","unstructured":"V. Padovani. Decidability of all minimal models. In S. Berardi and M. Coppo, editors, Types for Proof and Programs 1995, volume 1158 in Lecture Notes in Computer Science, pages 201\u2013215. Springer-Verlag, 1996."},{"key":"2_CR82","unstructured":"V. Padovani. Filtrage d\u2019ordre sup\u00e9rieur. Th\u00e8se de Doctorat, Universit\u00e9 de Paris VII, 1996."},{"key":"2_CR83","unstructured":"Larry C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and computer science, pages 361\u2013385. Academic Press, 1991."},{"key":"2_CR84","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Partial polymorphic type inference and higher-order unification. In Conference on Lisp and Functional Programming, pages 153\u2013163, 1988.","DOI":"10.1145\/62678.62697"},{"key":"2_CR85","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Logic programming in the LF logical framework. In G. Huet and G. Plotkin, editors, Logical frameworks, pages 149\u2013181. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"2_CR86","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Unification and anti-unification in the calculus of constructions. In Logic in Computer Science, pages 74\u201385, 1991.","DOI":"10.1109\/LICS.1991.151632"},{"key":"2_CR87","unstructured":"F. Pfenning and I. Cervesato. Linear higher-order pre-unification. In Logic in Computer Science, 1997."},{"key":"2_CR88","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Carsten Sch\u00fcrmann. System description: Twelf \u2014 A metalogical framework for deductive systems. In Proceedings of the 16th Int. Conference on Automated Deduction (CADE-16), volume 1632 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"2_CR89","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/321752.321764","volume":"20","author":"T. Pietrzykowski","year":"1973","unstructured":"T. Pietrzykowski. A complete mecanization of second-order type theory. J. of the Association for Computing Machinery, 20:333\u2013364, 1973.","journal-title":"J. of the Association for Computing Machinery"},{"key":"2_CR90","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin. Building-in equational theories. Machine Intelligence, 7:73\u201390, 1972.","journal-title":"Machine Intelligence"},{"key":"2_CR91","doi-asserted-by":"crossref","unstructured":"C. Prehofer. Decidable higher-order unification problems. In A. Bundy, editor, Conference on Automated Deduction, volume 814 of Lecture Notes in Artificial Intelligence, pages 635\u2013649. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_46"},{"key":"2_CR92","doi-asserted-by":"crossref","unstructured":"C. Prehofer. Higher-order narrowing. In Logic in Computer Science (LICS\u201994, pages 507\u2013516, 1994.","DOI":"10.1109\/LICS.1994.316040"},{"key":"2_CR93","volume-title":"Doctoral thesis","author":"C. Prehofer","year":"1995","unstructured":"C. Prehofer. Solving higher-order equations: From logic to programming. Doctoral thesis, Technische Universit\u00e4t M\u00fcnchen. Technical Report TUM-19508, Institut f\u00fcr Informatik, TUM, M\u00fcnchen, 1995."},{"key":"2_CR94","doi-asserted-by":"crossref","unstructured":"C. Prehofer. Solving Higher-Order Equations: From Logic to Programming. Progress in theoretical coputer science. Birkh\u00e4user, 1998.","DOI":"10.1007\/978-1-4612-1778-7"},{"key":"2_CR95","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1023\/A:1005394619746","volume":"20","author":"S. Pulman","year":"1997","unstructured":"S. Pulman. Higher-order unification and the interpretation of focus. Linguistics and Philosophy, 20:73\u2013115, 1997.","journal-title":"Linguistics and Philosophy"},{"key":"2_CR96","unstructured":"D. Pym. Proof, search, and computation in general logic. Doctoral thesis, University of Edinburgh, 1990."},{"key":"2_CR97","doi-asserted-by":"crossref","unstructured":"Z. Qian. Higher-order equational logic programming. In Principle of Programming Languages, pages 254\u2013267, 1994.","DOI":"10.1145\/174675.177889"},{"key":"2_CR98","unstructured":"Z. Qian and K. Wang. Higher-order equational E-unification for arbitrary theories. In K. Apt, editor, Joint International Conference and Symposium on Logic Programming, 1992."},{"key":"2_CR99","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BFb0016847","volume-title":"International Conference on Constaints in Computational Logic","author":"Z. Qian","year":"1994","unstructured":"Z. Qian and K. Wang. Modular AC unification of higher-order patterns. In J.-P. Jouannaud, editor, International Conference on Constaints in Computational Logic, volume 845 of Lecture Notes in Computer Science, pages 105\u2013120. Springer-Verlag, 1994."},{"key":"2_CR100","unstructured":"J.A. Robinson. New directions in mechanical theorem proving. In A.J.H. Morrell, editor, International Federation for Information Processing Congress, 1968, pages 63\u201367. North Holland, 1969."},{"key":"2_CR101","first-page":"123","volume":"5","author":"J.A. Robinson","year":"1970","unstructured":"J.A. Robinson. A note on mechanizing higher order logic. Machine Intelligence, 5:123\u2013133, 1970.","journal-title":"Machine Intelligence"},{"key":"2_CR102","unstructured":"H. Sa\u00efdi. R\u00e9solution d\u2019\u00e9quations dans le syst\u00e8me T de G\u00f6del. M\u00e9moire de DEA, Universit\u00e9 de Paris VII, 1994."},{"key":"2_CR103","volume-title":"Technical Report 12","author":"M. Schmidt-Schau\u00df","year":"1994","unstructured":"M. Schmidt-Schau\u00df. Unification of stratified second-order terms. Technical Report 12, J.W.Goethe-Universit\u00e4t, Frankfurt, 1994."},{"key":"2_CR104","volume-title":"Technical Report 11","author":"M. Schmidt-Schau\u00df","year":"1999","unstructured":"M. Schmidt-Schau\u00df. Decidability of bounded second order unification. Technical Report 11, J.W.Goethe-Universit\u00e4t, Frankfurt, 1999."},{"key":"2_CR105","doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schau\u00df and K.U. Schulz. Solvability of context equations with two context variables is decidable. In H. Ganzinger, editor, Conference on Automated Deduction, volume 1632 in Lecture Notes in Artificial Intelligence, pages 67\u201381, 1999.","DOI":"10.1007\/3-540-48660-7_5"},{"key":"2_CR106","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/BFb0030617","volume-title":"Theory and Practice of Software Development","author":"A. Schubert","year":"1997","unstructured":"A. Schubert. Linear interpolation for the higher order matching problem. In M. Bidoit and M. Dauchet, editors, Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer science, pages 441\u2013452. Springer-Verlag, 1997."},{"key":"2_CR107","doi-asserted-by":"crossref","unstructured":"A. Schubert. Second-order unification and type inference for Church-style polymorphism. In Principle of Programming Languages, pages 279\u2013288, 1998.","DOI":"10.1145\/268946.268969"},{"key":"2_CR108","doi-asserted-by":"crossref","unstructured":"W. Snyder. Higher-order E-unification. In M. E. Stickel, editor, Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence, pages 573\u2013587. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_115"},{"issue":"1 & 2","key":"2_CR109","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W. Snyder","year":"1989","unstructured":"W. Snyder and J. Gallier. Higher order unification revisited: Complete sets of tranformations. Journal of Symbolic Computation, 8(1 & 2):101\u2013140, 1989. Special issue on unification. Part two.","journal-title":"Journal of Symbolic Computation"},{"key":"2_CR110","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W. Snyder","year":"1989","unstructured":"W. Snyder and J. Gallier. Higher-order unification revisited: Complete sets of transformations. Journal of Symbolic Computation, 8:101\u2013140, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"2_CR111","unstructured":"J. Springintveld. Algorithms for type theory. Doctoral thesis, Utrecht University, 1995."},{"key":"2_CR112","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/BFb0014069","volume-title":"Typed Lambda Calculi and Applications","author":"J. Springintveld","year":"1995","unstructured":"J. Springintveld. Third-order matching in presence of type constructors. In M. Dezani-Ciancagliani and G. Plotkin, editors, Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 428\u2013442. Springer-Verlag, 1995."},{"key":"2_CR113","series-title":"Lect Notes Comput Sci","first-page":"221","volume-title":"Higher-order Algebra, Logic and Term Rewriting","author":"J. Springintveld","year":"1995","unstructured":"J. Springintveld. Third-order matching in the polymorphic lambda calculus. In G. Dowek, J. Heering, K. Meinke, and B. M\u00dfoller, editors, Higher-order Algebra, Logic and Term Rewriting, volume 1074 of Lecture Notes in Computer Science, pages 221\u2013237. Springer-Verlag, 1995."},{"key":"2_CR114","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/BF00632780","volume":"19","author":"F. C.N. P. Stuart","year":"1996","unstructured":"Fernando C.N. Pereira Stuart, M. Shieber, and Mary Dalrymple. Interactions of scope and ellipsis. Linguistics and Philosophy, 19:527\u2013552, 1996.","journal-title":"Linguistics and Philosophy"},{"key":"2_CR115","unstructured":"D.A. Wolfram. The clausal theory of types. Doctoral thesis, University of Cambridge, 1989."},{"key":"2_CR116","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/FI-1987-10304","volume":"X","author":"M. Zaionc","year":"1987","unstructured":"M. Zaionc. The regular expression description of unifier set in the typed \u03bb-calculus. Fundementa Informaticae, X:309\u2013322, 1987.","journal-title":"Fundementa Informaticae"},{"key":"2_CR117","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF00244393","volume":"4","author":"M. Zaionc","year":"1988","unstructured":"M. Zaionc. Mechanical procedure for proof construction via closed terms in typed \u03bb-calculus. Journal of Automated Reasoning, 4:173\u2013190, 1988.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T22:42:56Z","timestamp":1683844976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":117,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}