{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214510},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_33","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"408-422","source":"Crossref","is-referenced-by-count":5,"title":["Solving for Set Variables in Higher-Order Theorem Proving"],"prefix":"10.1007","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"33_CR1","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_CR2","doi-asserted-by":"crossref","unstructured":"Peter B. Andrews. Classical type theory. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume 2, chapter 15, pages 965\u20131007. Elsevier Science, 2001.","DOI":"10.1016\/B978-044450813-3\/50017-5"},{"key":"33_CR3","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_CR4","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 (1994), 411\u2013412.","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR5","unstructured":"F. Bartels, A. Dold, F. W. v. Henke, H. Pfeifer, and H. Rue\u00df. Formalizing Fixed-Point Theory in PVS. Ulmer Informatik-Berichte 96-10, Universit\u00e4t Ulm, Fakult\u00e4t f\u00fcr Informatik, 1996."},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Christoph Benzm\u00fcller and Michael Kohlhase. System description: LEO \u2014 a higher-order theorem prover. 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 139\u2013143, Lindau, Germany, 1998. Springer-Verlag.","DOI":"10.1007\/BFb0054256"},{"key":"33_CR7","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W. Bibel","year":"1983","unstructured":"Wolfgang Bibel. Matings in matrices. Communications of the ACM, 26:844\u2013852, 1983.","journal-title":"Communications of the ACM"},{"key":"33_CR8","first-page":"53","volume-title":"Machine Intelligence","author":"W. W. Bledsoe","year":"1979","unstructured":"W. W. Bledsoe. A maximal method for set variables in automatic theorem proving. In J. E. Hayes, Donald Michie, and L. I. Mikulich, editors, Machine Intelligence 9, pages 53\u2013100. Ellis Harwood Ltd., Chichester, and John Wiley & Sons, 1979."},{"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 Guohui Feng. Set-Var. Journal of Automated Reasoning, 11:293\u2013314, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR10","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":"33_CR11","doi-asserted-by":"crossref","unstructured":"Amy Felty. Proof search with set variable instantiation in the calculus of constructions. In M. A. McRobbie and J. K. Slaney, editors, Automated Deduction: CADE-13, volume 1104 of Lecture Notes in Artificial Intelligence, pages 658\u2013672. Springer, 1996.","DOI":"10.1007\/3-540-61511-3_120"},{"key":"33_CR12","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(99)00175-9","volume":"232","author":"A. Felty","year":"2000","unstructured":"Amy Felty. The calculus of constructions as a framework for proof search with set variable instantiation. Theoretical Computer Science, 232:187\u2013229, 2000.","journal-title":"Theoretical Computer Science"},{"key":"33_CR13","first-page":"139","volume-title":"The Curry-Howard Isomorphism","author":"J. H. Geuvers","year":"1995","unstructured":"J. H. Geuvers. The calculus of constructions and higher order logic. In Ph. de Groote, editor, The Curry-Howard Isomorphism, pages 139\u2013191. Academia, Louvain-la-Neuve (Belgium), 1995."},{"key":"33_CR14","unstructured":"Sunil Issar. Operational Issues in Automated Theorem Proving Using Matings. PhD thesis, Carnegie Mellon University, 1991. 147 pp."},{"key":"33_CR15","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."},{"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":"crossref","unstructured":"Neil V. Murray and Erik Rosenthal. Dissolution: Making paths vanish. Journal of the ACM, 40(3):504\u2013535, July 1993.","DOI":"10.1145\/174130.174135"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"H. J. Ohlbach. SCAN\u2014elimination of predicate quantifiers. In M. A. McRobbie and J. K. Slaney, editors, Automated Deduction: CADE-13, volume 1104 of Lecture Notes in Artificial Intelligence, pages 161\u2013165. Springer, 1996.","DOI":"10.1007\/3-540-61511-3_77"},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In Alan Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 148\u2013161, Nancy, France, June 1994. Springer-Verlag LNAI 814.","DOI":"10.1007\/3-540-58156-1_11"},{"issue":"2","key":"33_CR20","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF00881916","volume":"15","author":"L. C. Paulson","year":"1995","unstructured":"Lawrence C. Paulson. Set theory for verification: II. Induction and recursion. Journal of Automated Reasoning, 15(2):167\u2013215, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"33_CR21","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation, 7(2):175\u2013204, March 1997.","DOI":"10.1093\/logcom\/7.2.175"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:55:50Z","timestamp":1556754950000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_33","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}