{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:40Z","timestamp":1749124060695},"publisher-location":"Berlin\/Heidelberg","reference-count":6,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012870","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"714-729","source":"Crossref","is-referenced-by-count":2,"title":["Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programs"],"prefix":"10.1007","author":[{"given":"Larry","family":"Wos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William","family":"McCune","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"51_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":"51_CR2","volume-title":"Combinatory Logic I","author":"H. B. Curry","year":"1958","unstructured":"Curry, H. B., and Feys, R., Combinatory Logic I, North-Holland, Amsterdam (1958)."},{"key":"51_CR3","volume-title":"Combinatory Logic II","author":"H. B. Curry","year":"1972","unstructured":"Curry, H. B., Hindley, J. R., and Seldin, J. P., Combinatory Logic II, North-Holland, Amsterdam (1972)."},{"key":"51_CR4","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"C-25","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R., and Wos, L., \u201cProblems and experiments for and with automated theorem proving programs\u201d, IEEE Transactions on Computers\nC-25, pp. 773\u2013782 (1976).","journal-title":"IEEE Transactions on Computers"},{"key":"51_CR5","first-page":"135","volume-title":"Machine Intelligence 4","author":"G. Robinson","year":"1969","unstructured":"Robinson, G., and Wos, L., \u201cParamodulation and theorem-proving in first-order theories with equality\u201d, pp. 135\u2013150 in Machine Intelligence 4, ed. B. Meltzer and D. Michie, Edinburgh University Press, Edinburgh (1969)."},{"key":"51_CR6","unstructured":"Smullyan, R., To Mock a Mockingbird, Alfred A. Knopf, New York (1985)."}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012870.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:06:46Z","timestamp":1607353606000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012870"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/bfb0012870","relation":{},"subject":[]}}