{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:46:18Z","timestamp":1725486378240},"publisher-location":"Berlin, Heidelberg","reference-count":6,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540429579"},{"type":"electronic","value":"9783540456537"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45653-8_21","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T04:57:30Z","timestamp":1181365050000},"page":"309-319","source":"Crossref","is-referenced-by-count":2,"title":["First-Order Atom Definitions Extended"],"prefix":"10.1007","author":[{"given":"Bijan","family":"Afshordel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Hillenbrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,11,20]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. Stratified resolution. In D. McAllester, editor, 17th International Conference on Automated Deduction (CADE-17), volume 1831, pages 365\u2013384, Pittsburgh, 2000.","key":"21_CR1","DOI":"10.1007\/10721959_28"},{"doi-asserted-by":"crossref","unstructured":"Andreas Nonnengart, Georg Rock, and Christoph Weidenbach. On generating small clause normal forms. In Claude Kirchner and H\u00e9l\u00e8ne Kirchner, editors, 15th International Conference on Automated Deduction, CADE-15, volume 1421 of LNAI, pages 397\u2013411. Springer, 1998.","key":"21_CR2","DOI":"10.1007\/BFb0054274"},{"doi-asserted-by":"crossref","unstructured":"David A. Plaisted and Yunshan Zhu. Replacement rules with definition detection. In Ricardo Caferra and Gernot Salzer, editors, Automated Deduction in Classical and Non-Classical Logics, volume 1761 of LNAI, pages 80\u201394. Springer, 1998.","key":"21_CR3","DOI":"10.1007\/3-540-46508-1_5"},{"key":"21_CR4","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-58156-1_18","volume-title":"Twelfth International Conference on Automated Deduction, CADE-12","author":"G. Sutcliffe","year":"1994","unstructured":"Geoff Sutcliffe, Christian B. Suttner, and Theodor Yemenis. The TPTP problem library. In Alan Bundy, editor, Twelfth International Conference on Automated Deduction, CADE-12, volume 814 of LNAI, pages 252\u2013266, Nancy, France, June 1994. Springer."},{"doi-asserted-by":"crossref","unstructured":"Christoph Weidenbach. Combining Superposition, Sorts and Splitting. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, chapter 27, pages 1965\u20132013. Elsevier Science Publishers B.V., 2001.","key":"21_CR5","DOI":"10.1016\/B978-044450813-3\/50029-1"},{"unstructured":"Larry Wos. Automated Reasoning, 33 Basic Research Problems. Prentice Hall, 1988.","key":"21_CR6"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45653-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T23:20:49Z","timestamp":1556493649000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45653-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540429579","9783540456537"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/3-540-45653-8_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}