{"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":1749124060535},"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\/bfb0012868","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"704-709","source":"Crossref","is-referenced-by-count":2,"title":["Challenge equality problems in lattice theory"],"prefix":"10.1007","author":[{"given":"William","family":"McCune","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"49_CR1","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1017\/S2040618500035103","volume":"7","author":"R. Bumcroft","year":"1965","unstructured":"Bumcroft, R., Proc. Glasgow Math. Assoc. 7, Pt. 1, pp.22\u201323 (1965).","journal-title":"Proc. Glasgow Math. Assoc."},{"key":"49_CR2","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/321495.321500","volume":"16","author":"J. Guard","year":"1969","unstructured":"Guard, J., Oglesby, F., Bennett, J., and Settle, L., \u201cSemi-automated mathematics\u201d, Journal of the ACM\n16, pp. 49\u201362 (1969).","journal-title":"Journal of the ACM"},{"key":"49_CR3","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-18088-5_6","volume":"267","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J., and Rusinowitch, M., \u201cOn word problems in equational theories\u201d, in Proceedings of the 14th International Colloquium on Languages, Automata, and Programming, Springer-Verlag Lecture Notes in Computer Science, Vol. 267, pp. 54\u201371 (1987).","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"49_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0898-1221(76)90002-X","volume":"2","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R., and Wos, L., \u201cComplexity and related enhancements for automated theorem-proving programs\u201d, Computers and Mathematics with Applications\n2, pp. 1\u201316 (1976).","journal-title":"Computers and Mathematics with Applications"},{"key":"49_CR5","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. E. Peterson","year":"1983","unstructured":"Peterson, G. E., \u201cA technique for establishing completeness results in theorem proving with equality\u201d, SIAM Journal of Computing\n12, pp. 82\u2013100 (1983).","journal-title":"SIAM Journal of Computing"},{"key":"49_CR6","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)."}],"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\/BFb0012868.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:06:45Z","timestamp":1607353605000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012868"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/bfb0012868","relation":{},"subject":[]}}