{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:03Z","timestamp":1749124083445},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_46","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:23:04Z","timestamp":1330251784000},"page":"635-649","source":"Crossref","is-referenced-by-count":10,"title":["Decidable higher-order unification problems"],"prefix":"10.1007","author":[{"given":"Christian","family":"Prehofer","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"46_CR1","doi-asserted-by":"crossref","unstructured":"Peter B. Andrews, Sunil Issar, Dan Nesmith, and Frank Pfenning. The TPS theorem proving system. In M.E. Stickel, editor, Proc. 10th Int. Conf. Automated Deduction, pages 641\u2013642. LNCS 449, 1990.","DOI":"10.1007\/3-540-52885-7_120"},{"key":"46_CR2","unstructured":"Hendrik Pieter Barendregt. The Lambda Calculus, its Syntax and Semantics. North Holland, 2nd edition, 1984."},{"key":"46_CR3","volume-title":"PhD thesis","author":"L. D. Baxter","year":"1976","unstructured":"L. D. Baxter. The complexity of Unification. PhD thesis, University of Waterloo, Waterloo, Canada, 1976."},{"key":"46_CR4","volume-title":"Implementing Mathematics With the Nuprl Proof Development System","author":"R. Constable","year":"1986","unstructured":"Robert Constable, S. Allen, H. Bromly, W. Cleaveland, J. Cremer, R. Harper, D. Howe, T. Knoblock, N. Mendler, P. Panangaden, J. Sasaki, and S. Smith. Implementing Mathematics With the Nuprl Proof Development System. Prentice-Hall, New Jersey, 1986."},{"key":"46_CR5","doi-asserted-by":"crossref","unstructured":"R\u00e9gis Curien. Second-order E-matching as a tool for automated theorem proving. In EPIA '93. Springer LNCS 725, 1993.","DOI":"10.1007\/3-540-57287-2_51"},{"key":"46_CR6","doi-asserted-by":"crossref","unstructured":"Michael R. Donat and Lincoln A. Wallen. Learning and applying generalised solutions using higher order resolution. In E. Lusk and R. Overbeek, editors, 9th International Conference On Automated Deduction, pages 41\u201361. Springer Verlag, 1988.","DOI":"10.1007\/BFb0012822"},{"key":"46_CR7","first-page":"2","volume-title":"Third order matching is decidable","author":"G. Dowek","year":"1992","unstructured":"Gilles Dowek. Third order matching is decidable. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 2\u201310, Santa Cruz, California, 22\u201325 June 1992. IEEE Computer Society Press."},{"key":"46_CR8","unstructured":"Gilles Dowek. Personal communication, 1993."},{"key":"46_CR9","doi-asserted-by":"crossref","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":"46_CR10","doi-asserted-by":"crossref","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 undecideable. Theoretical Computer Science, 87:25\u201341, 1991.","journal-title":"Theoretical Computer Science"},{"key":"46_CR11","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1989."},{"key":"46_CR12","doi-asserted-by":"crossref","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":"46_CR13","unstructured":"Masami Hagiya. Synthesis of rewrite programs by higher-order semantic unification. In S. Arikawa, S. Goto, S. Ohsuga, and T. Yokomori, editors, Algorithmic Learning Theory, pages 396\u2013410. Springer, 1990."},{"key":"46_CR14","unstructured":"Masateru Harao. Analogical reasoning based on higher-order unification. In S. Arikawa, S. Goto, S. Ohsuga, and T. Yokomori, editors, Algorithmic Learning Theory, pages 151\u2013163. Springer, 1990."},{"key":"46_CR15","unstructured":"J.R. Hindley and Jonathan P. Seldin. Introduction to Combinators and \u03bb-Calculus. Cambridge University Press, 1986."},{"key":"46_CR16","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G\u00e9rard Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"46_CR17","unstructured":"G\u00e9rard Huet. R\u00e9solution d'\u00e9quations dans les languages d'ordre 1,2,...\u03a9. PhD thesis, University Paris-7, 1976."},{"key":"46_CR18","doi-asserted-by":"crossref","unstructured":"Jean-Marie Hullot. Canonical forms and unification. In W. Bibel and R. Kowalski, editors, Proceedings of 5th Conference on Automated Deduction, pages 318\u2013334. Springer Verlag, LNCS, 1980.","DOI":"10.21236\/ADA087640"},{"key":"46_CR19","series-title":"LNCS","first-page":"216","volume-title":"Computer Science Logic. Selected papers from CSL'92","author":"M. Rodr\u00edguez-Artalejo","year":"1992","unstructured":"M. Rodr\u00edguez-Artalejo J.C. Gonz\u00e1lez-Moreno, M.T. Hortal\u00e1-Gonz\u00e1lez. On the completeness of narrowing as the operational semantics of functional logic programming. In E. B\u00f6rger, G. J\u00e4ger, H. Kleine B\u00fcning, S. Martini, and M.M. Richter, editors, Computer Science Logic. Selected papers from CSL'92, LNCS, pages 216\u2013231, San Miniato, Italy, September 1992. Springer."},{"key":"46_CR20","volume-title":"Technical Report CSRR 2059","author":"C. L. Lucchesi","year":"1972","unstructured":"C. L. Lucchesi. The undecidability of the unification problem for third order languages. Technical Report CSRR 2059, University of Waterloo, Waterloo, Canada, 1972."},{"key":"46_CR21","unstructured":"Dale Miller. Unification of simply typed lambda-terms as logic programming. In P.K. Furukawa, editor, Proc. 1991 Joint Int. Conf. Logic Programming, pages 253\u2013281. MIT Press, 1991."},{"key":"46_CR22","unstructured":"Gopalan Nadathur and Dale Miller. An overview of \u03bb-Prolog. In Robert A. Kowalski and Kenneth A. Bowen, editors, Proc. 5th Int. Logic Programming Conference, pages 810\u2013827. MIT Press, 1988."},{"key":"46_CR23","volume-title":"Technical report","author":"P. Narendran","year":"1989","unstructured":"P. Narendran. Some remarks on second order unification. Technical report, Institute of Programming and Logics, Dep. of Computer Science, State Univ. of New York at Albany, 1989."},{"key":"46_CR24","first-page":"342","volume-title":"Higher-order critical pairs","author":"T. Nipkow","year":"1991","unstructured":"Tobias Nipkow. Higher-order critical pairs. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 342\u2013349, Amsterdam, The Netherlands, 15\u201318 July 1991. IEEE Computer Society Press."},{"key":"46_CR25","unstructured":"Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361\u2013385. Academic Press, 1990."},{"key":"46_CR26","first-page":"153","volume-title":"Partial polymorphic type inference and higher-order unification","author":"F. Pfenning","year":"1988","unstructured":"F. Pfenning. Partial polymorphic type inference and higher-order unification. In ACM Conference on Lisp and Functional Programming, pages 153\u2013163, Snowbird, Utah, July 1988. ACM-Press."},{"key":"46_CR27","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Logic programming in the LF logical framework. In G\u00e9rard Huet and Gordon D. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"46_CR28","doi-asserted-by":"crossref","unstructured":"Christian Prehofer. Higher-order narrowing. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1994. To appear.","DOI":"10.1109\/LICS.1994.316040"},{"key":"46_CR29","first-page":"3","volume-title":"Logic Programming: Functions, Relations, and Equations","author":"U. S. Reddy","year":"1986","unstructured":"U. S. Reddy. On the relationship between logic and functional languages. In D. DeGroot and G. Lindstrom, editors, Logic Programming: Functions, Relations, and Equations, pages 3\u201336. Prentice-Hall, Englewood Cliffs, NJ, 1986."},{"key":"46_CR30","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W. Snyder","year":"1989","unstructured":"Wayne Snyder and Jean Gallier. Higher-order unification revisited: Complete sets of transformations. J. Symbolic Computation, 8:101\u2013140, 1989.","journal-title":"J. Symbolic Computation"},{"key":"46_CR31","doi-asserted-by":"crossref","unstructured":"D. A. Wolfram. The Clausal Theory of Types. Cambridge Tracts in Theoretical Computer Science 21. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9780511569906"},{"key":"46_CR32","unstructured":"J.-H. You. Enumerating outer narrowing derivation for constructor-based term rewriting systems. In C. Kirchner, editor, Unification, pages 541\u2013564. Academic Press, 1990. Also in J. Symbolic Computation, 1989."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_46.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:17:41Z","timestamp":1605629861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}