{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:05Z","timestamp":1749124085858},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540528852"},{"type":"electronic","value":"9783540471714"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52885-7_109","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:45:32Z","timestamp":1330206332000},"page":"485-499","source":"Crossref","is-referenced-by-count":15,"title":["Automated reasoning contributes to mathematics and logic"],"prefix":"10.1007","author":[{"given":"L.","family":"Wos","sequence":"first","affiliation":[]},{"given":"S.","family":"Winker","sequence":"additional","affiliation":[]},{"given":"W.","family":"McCune","sequence":"additional","affiliation":[]},{"given":"R.","family":"Overbeek","sequence":"additional","affiliation":[]},{"given":"E.","family":"Lusk","sequence":"additional","affiliation":[]},{"given":"R.","family":"Stevens","sequence":"additional","affiliation":[]},{"given":"R.","family":"Butler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"35_CR1","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H.P. Barendregt","year":"1981","unstructured":"Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics, North-Holland, Amsterdam, 1981."},{"key":"35_CR2","volume-title":"Cylindric Algebras, Part I","author":"L. Henkin","year":"1971","unstructured":"Henkin, L., J. Monk, and A. Tarski. Cylindric Algebras, Part I, North-Holland, Amsterdam, 1971."},{"key":"35_CR3","first-page":"274","volume":"35","author":"E. Huntington","year":"1933","unstructured":"Huntington, E. New sets of independent postulates for the algebra of logic, with special reference to Whitehead and Russell's Principia Mathematica, Trans. of AMS 35 (1933), 274\u2013304.","journal-title":"Trans. of AMS"},{"issue":"1","key":"35_CR4","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BF02575007","volume":"36","author":"E. Lusk","year":"1987","unstructured":"Lusk E. and R. McFadden. Using automated reasoning tools: a study of the semigroup {F2B2}, Semigroup Forum 36, 1 (1987), 75\u201388.","journal-title":"Semigroup Forum"},{"key":"35_CR5","unstructured":"McCune, W. OTTER 2.0 Users Guide, Argonne National Laboratory Report ANL-90\/9, 1990."},{"key":"35_CR6","first-page":"496","volume":"170","author":"H.-J. Ohlbach","year":"1984","unstructured":"Ohlbach, H.-J. and G. Wrightson. Solving a problem in relevance logic with an automated theorem prover, Proc. of CADE-7, Springer-Verlag Lecture Notes in Computer Science, Vol. 170, ed. R. Shostak, New York, 1984, 496\u2013508.","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"35_CR7","unstructured":"Peterson J. The Possible Shortest Single Axioms for EC-Tautologies, Aukland University Department of Mathematics Report Series No. 105, 1977."},{"key":"35_CR8","first-page":"710","volume":"310","author":"F. Pfenning","year":"1988","unstructured":"Pfenning, F. Single axioms in the implicational propositional calculus, Proc. of CADE-9, Springer-Verlag Lecture Notes in Computer Science, Vol. 310, ed. E. Lusk and R. Overbeek, New York, 1988, 710\u2013713.","journal-title":"Proc. of CADE-9"},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"Slaney, J. K. and E. Lusk. Parallelizing the closure computation in automated deduction, to appear in the proceedings of CADE-10, 1990.","DOI":"10.1007\/3-540-52885-7_77"},{"key":"35_CR10","volume-title":"To Mock a Mockingbird","author":"R. Smullyan","year":"1985","unstructured":"Smullyan, R. To Mock a Mockingbird, A. Knopf, New York, 1985."},{"key":"35_CR11","volume-title":"Automated Reasoning: Introduction and Applications","author":"L. Wos","year":"1984","unstructured":"Wos, L., R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning: Introduction and Applications, Prentice-Hall, New York, 1984."},{"key":"35_CR12","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0004-3702(84)90054-7","volume":"22","author":"L. Wos","year":"1984","unstructured":"Wos, L., S. Winker, B. Smith, R. Veroff, and L. Henschen. A new use of an automated reasoning assistant: open questions in equivalential calculus and the study of infinite domains, Artificial Intelligence 22 (1984), 303\u2013356.","journal-title":"Artificial Intelligence"},{"key":"35_CR13","volume-title":"Subsumption, a sometimes undervalued procedure, preprint MCS-P93-0789","author":"L. Wos","year":"1989","unstructured":"Wos, L., R. Overbeek, and E. Lusk. Subsumption, a sometimes undervalued procedure, preprint MCS-P93-0789, Argonne National Laboratory, Argonne, Ill., July 1989."},{"key":"35_CR14","unstructured":"Wos, L., S. Winker, W. McCune, R. Overbeek, E. Lusk, R. Stevens, and R. Butler. OTTER Experiments Pertinent to CADE-10, Argonne National Laboratory Report ANL-89\/39, to appear."}],"container-title":["Lecture Notes in Computer Science","10th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52885-7_109.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:28Z","timestamp":1605648328000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52885-7_109"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540528852","9783540471714"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-52885-7_109","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}