{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:56Z","timestamp":1761611216352},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_32","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T20:53:07Z","timestamp":1194641587000},"page":"359-373","source":"Crossref","is-referenced-by-count":6,"title":["A Breadth-First Strategy for Mating Search"],"prefix":"10.1007","author":[{"given":"Matthew","family":"Bishop","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"32_CR1","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P. B. Andrews","year":"1996","unstructured":"Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi. TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning, 16:321\u2013353, 1996.","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR2","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. B. Andrews","year":"1981","unstructured":"Peter B. Andrews. Theorem proving via general matings. Journal of the ACM, 28:193\u2013214, 1981.","journal-title":"Journal of the ACM"},{"key":"32_CR3","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BF00248320","volume":"5","author":"P. B. Andrews","year":"1989","unstructured":"Peter B. Andrews. On connections and higher-order logic. Journal of Automated Reasoning, 5:257\u2013291, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Matthew Bishop and Peter B. Andrews. Selectively instantiating definitions. In Claude Kirchner and H\u00e9l\u00e8ne Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction, volume 1421 of Lecture Notes in Artificial Intelligence, pages 365\u2013380, Lindau, Germany, 1998. Springer-Verlag.","DOI":"10.1007\/BFb0054272"},{"key":"32_CR5","unstructured":"H. P. Barendregt. The \u03bb-Calculus. Studies in logic and the foundations of mathematics, North-Holland, 1984."},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"W. Bibel, S. Bruning, U. Egly, D. Korn, and T. Rath. Issues in theorem proving based on the connection method. In Peter Baumgartner, Reiner H\u00e4hnle, and Joachim Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods. 4th International Workshop. TABLEAUX\u2019 95, volume 918 of Lecture Notes in Artificial Intelligence, pages 1\u201316, Schlo\u00df Rheinfels, St. Goar, Germany, May 1995. Springer-Verlag.","DOI":"10.1007\/3-540-59338-1_24"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Wolfgang Bibel. Automated Theorem Proving. Vieweg, Braunschweig, 1982.","DOI":"10.1007\/978-3-322-90100-2"},{"key":"32_CR8","unstructured":"Matthew Bishop. Mating Search Without Path Enumeration. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, 1999."},{"key":"32_CR9","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF02328452","volume":"2","author":"R. Boyer","year":"1986","unstructured":"Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and Lawrence Wos. Set theory in first-order logic: Clauses for G\u00f6del\u2019s axioms. Journal of Automated Reasoning, 2:287\u2013327, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR10","unstructured":"S. Br\u00fcning. Techniques for Avoiding Redundancy in Theorem Proving Based on the Connection Method. PhD thesis, TH Darmstadt, 1994."},{"issue":"8","key":"32_CR11","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"32_CR12","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"32_CR13","doi-asserted-by":"publisher","first-page":"472","DOI":"10.2307\/1989762","volume":"3","author":"A. Church","year":"1936","unstructured":"Alonzo Church and J.B. Rosser. Some properties of conversion. Transactions of the American Mathematical Society, 3:472\u2013482, 1936.","journal-title":"Transactions of the American Mathematical Society"},{"key":"32_CR14","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W. D. Goldfarb","year":"1981","unstructured":"Warren D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225\u2013230, 1981.","journal-title":"Theoretical Computer Science"},{"key":"32_CR15","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"G. P. Huet","year":"1973","unstructured":"Gerard P. Huet. The undecidability of unification in third-order logic. Information and Control, 22:257\u2013267, 1973.","journal-title":"Information and Control"},{"key":"32_CR16","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. P. Huet","year":"1975","unstructured":"Gerard P. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"32_CR17","first-page":"221","volume":"1","author":"S. Issar","year":"1990","unstructured":"Sunil Issar. Path-focused duplication: A search procedure for general matings. In AAAI-90. Proceedings of the Eighth National Conference on Artificial Intelligence, volume 1, pages 221\u2013226. AAAI Press\/The MIT Press, 1990.","journal-title":"AAAI-90"},{"key":"32_CR18","unstructured":"Sunil Issar. Operational Issues in Automated Theorem Proving Using Matings. PhD thesis, Carnegie Mellon University, 1991. 147 pp."},{"key":"32_CR19","first-page":"133","volume":"6","author":"B. Knaster","year":"1927","unstructured":"B. Knaster. Une th\u00e9or\u00e8me sur les fonctions d\u2019ensembles. Annales Soc. Polonaise Math., 6:133\u2013134, 1927.","journal-title":"Annales Soc. Polonaise Math."},{"key":"32_CR20","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF00247825","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"Shie-Jue Lee and David A. Plaisted. Eliminating duplication with the hyperlinking strategy. Journal of Automated Reasoning, 9:25\u201342, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"32_CR21","unstructured":"Frank Pfenning. Proof Transformations in Higher-Order Logic. PhD thesis, Carnegie Mellon University, 1987. 156 pp."},{"key":"32_CR22","doi-asserted-by":"publisher","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. Journal of Symbolic Computation, 8:101\u2013140, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"32_CR23","volume-title":"Introduction to Lattice Theory","author":"G. Sz\u00e1sz","year":"1963","unstructured":"Gabor Sz\u00e1sz. Introduction to Lattice Theory. Academic Press, New York and London, 1963."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T08:56:30Z","timestamp":1556960190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_32","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}