{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:08:52Z","timestamp":1761620932179,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054272","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"365-380","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Selectively instantiating definitions"],"prefix":"10.1007","author":[{"given":"Matthew","family":"Bishop","sequence":"first","affiliation":[]},{"given":"Peter B.","family":"Andrews","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"33_CR1","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":"33_CR2","unstructured":"Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986."},{"key":"33_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":"33_CR4","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":"33_CR5","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/BF00881874","volume":"11","author":"S. C. Bailin","year":"1993","unstructured":"Sidney C. Bailin and Dave Barker-Plummer. Z-match: An Inference Rule for Incrementally Elaborating Set Instantiations. Journal of Automated Reasoning, 11:391\u2013428, 1993. Errata: JAR 12:411\u2013412, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR6","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BF02341853","volume":"8","author":"D. Barker-Plummer","year":"1992","unstructured":"Dave Barker-Plummer. Gazing: An Approach to the Problem of Definition and Lemma Use. Journal of Automated Reasoning, 8:311\u2013344, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR7","unstructured":"W. W. Bledsoe. Using Examples to Generate Instantiations of Set Variables. In Proceedings of IJCAI-83, Karlsruhe, Germany, pages 892\u2013901, Aug 8\u201312, 1983."},{"issue":"1","key":"33_CR8","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0004-3702(74)90009-5","volume":"5","author":"W. W. Bledsoe","year":"1974","unstructured":"W. W. Bledsoe and Peter Bruell. A Man-Machine Theorem-Proving System. Artificial Intelligence, 5(1):51\u201372, 1974.","journal-title":"Artificial Intelligence"},{"key":"33_CR9","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BF00881869","volume":"11","author":"W. W. Bledsoe","year":"1993","unstructured":"W. W. Bledsoe and Gohui Feng. Set-Var. Journal of Automated Reasoning, 11:293\u2013314, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR10","first-page":"56","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church. A Formulation of the Simple Theory of Types. Journal of Symbolicogic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolicogic"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Fausto Giunchiglia and Adolfo Villafiorita. ABSFOL: a Proof Checker with Abstraction. In M.A. McRobbie and J.K. Slaney, editors, CADE-13: Proceedings of the 13th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 1104, pages 136\u2013140. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61511-3_74"},{"key":"33_CR12","unstructured":"Fausto Giunchiglia and Toby Walsh. Theorem Proving with Definitions. In Proceedings of AISB 89, Society for the Study of Artificial Intelligence and Simulation of Behaviour, 1989."},{"issue":"2\u20133","key":"33_CR13","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0004-3702(92)90021-O","volume":"57","author":"F. Giunchiglia","year":"1992","unstructured":"Fausto Giunchiglia and Toby Walsh. A Theory of Abstraction. Artificial Intelligence, 57(2\u20133):323\u2013389, 1992.","journal-title":"Artificial Intelligence"},{"key":"33_CR14","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":"33_CR15","doi-asserted-by":"publisher","first-page":"906","DOI":"10.2307\/2312410","volume":"71","author":"I. I. Kolodner","year":"1964","unstructured":"Ignace I. Kolodner. Fixed Points. American Mathematical Monthly, 71:906, 1964.","journal-title":"American Mathematical Monthly"},{"issue":"4","key":"33_CR16","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BF00370646","volume":"46","author":"D. A. Miller","year":"1987","unstructured":"Dale A. Miller. A compact representation of proofs. Studia Logica, 46(4):347\u2013370, 1987.","journal-title":"Studia Logica"},{"key":"33_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(78)90028-0","volume":"10","author":"D. Pastre","year":"1978","unstructured":"D. Pastre. Automatic Theorem Proving in Set Theory. Artificial Intelligence, 10:1\u201327, 1978","journal-title":"Artificial Intelligence"},{"key":"33_CR18","unstructured":"Frank Pfenning. Proof Transformations in Higher-Order Logic. PhD thesis, Carnegie Mellon University, 1987. 156 pp."},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"D.A. Plaisted. Abstraction Mappings in Mechanical Theorem Proving. In 5th Conference on Automated Deduction, Lecture Notes in Computer Science 87, pages 264\u2013280. Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10009-1_21"},{"key":"33_CR20","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0004-3702(81)90015-1","volume":"16","author":"D.A. Plaisted","year":"1981","unstructured":"D.A. Plaisted. Theorem Proving with Abstraction. Artificial Intelligence, 16:47\u2013108, 1981.","journal-title":"Artificial Intelligence"},{"key":"33_CR21","unstructured":"Dave Plummer. Gazing: Controlling the Use of Rewrite Rules. PhD thesis, Dept. of Artificial Intelligence, University of Edinburgh, 1987."},{"key":"33_CR22","unstructured":"K. Warren. Implementation of a Definition Expansion Mechanism in a Connection Method Theorem Prover. Master's thesis, Dept. of Artificial Intelligence, Univ. of Edinburgh, 1987."},{"key":"33_CR23","first-page":"433","volume":"3","author":"L. Wos","year":"1987","unstructured":"Larry Wos. The Problem of Definition Expansion and Contraction. Journal of Automated Reasoning, 3:433\u2013435, 1987.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054272","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,18]],"date-time":"2023-01-18T20:05:23Z","timestamp":1674072323000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0054272"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0054272","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"25 May 2006","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}