{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:51:13Z","timestamp":1725573073760},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540252368"},{"type":"electronic","value":"9783540322757"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32275-7_10","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T21:14:41Z","timestamp":1292879681000},"page":"142-153","source":"Crossref","is-referenced-by-count":1,"title":["On a Semantic Subsumption Test"],"prefix":"10.1007","author":[{"given":"Jerzy","family":"Marcinkowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Otop","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grzegorz","family":"Stelmaszek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"10_CR1","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/BF00881866","volume":"10","author":"J. Christian","year":"1993","unstructured":"Christian, J.: Flat terms, discrimination nets, and fast term rewriting. Journal of Automated Reasoning\u00a010(1), 95\u2013113 (1993)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR2","unstructured":"EQP Equational Prover, \n                  \n                    http:\/\/www-unix.mcs.anl.gov\/AR\/eqp\/"},{"key":"10_CR3","unstructured":"Greenbaum, S.: Input transformations and resolution implementation techniques for theorem proving in first order logic, PhD thesis, Univ. of Illinois, at Urbana Champaign (1986)"},{"issue":"3","key":"10_CR4","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins Problem. Journal of Automated Reasoning\u00a019(3), 263\u2013276 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR5","unstructured":"Otter: An Automated Deduction System, \n                  \n                    http:\/\/www-unix.mcs.anl.gov\/AR\/otter\/"},{"key":"10_CR6","unstructured":"The TPTP (Thousands of Problems for Theorem Provers) Problem Library for Automated Theorem Proving by Geoff Sutcliffe and Christian Suttner, \n                  \n                    http:\/\/www.cs.miami.edu\/~tptp\/"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Sekar, R., Ramakrishnan, I.V., Voronkov, A.: Term Indexing. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, Elsevier\/MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"issue":"2","key":"10_CR8","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF00881918","volume":"15","author":"A. Voronkov","year":"1995","unstructured":"Voronkov, A.: The anatomy of vampire: implementing bottom-up procedures with code trees. Journal of Automated Reasoning\u00a015(2), 237\u2013265 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR9","unstructured":"http:\/\/www.cs.man.ac.uk\/~riazanoa\/Vampire\/\n                  \n                  \n                 and \n                  \n                    http:\/\/www.prover.info\/"}],"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\/978-3-540-32275-7_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:46:52Z","timestamp":1620013612000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32275-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540252368","9783540322757"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32275-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}