{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:09:45Z","timestamp":1725458985395},"publisher-location":"Berlin, Heidelberg","reference-count":5,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540188346"},{"type":"electronic","value":"9783540481904"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/bfb0035864","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:40:10Z","timestamp":1138203610000},"page":"395-396","source":"Crossref","is-referenced-by-count":0,"title":["Some tools for an inference laboratory (ATINF)"],"prefix":"10.1007","author":[{"given":"Thierry Boy","family":"de la Tour","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ricardo","family":"Caferra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gilles","family":"Chaminade","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,23]]},"reference":[{"key":"39_CR1","unstructured":"E. Eder: \"An implementation of a theorem prover based on the connection method\". Proc. AIMSA'84. Varna, Bulgaria, September 1984. North-Holland, 121\u2013128."},{"key":"39_CR2","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. Plaisted","year":"1986","unstructured":"D. Plaisted: \"A structure preserving clause form translation\". Journal of Symbolic Computation (1986) 2, 293\u2013304.","journal-title":"Journal of Symbolic Computation"},{"key":"39_CR3","doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schauss: \"Unification in many sorted equational theories\". Proc. 8th. CADE, Oxford, England, July 1986, 538\u2013552.","DOI":"10.1007\/3-540-16780-3_118"},{"issue":"4","key":"39_CR4","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"M. Stickel: \"Automated deduction by theory resolution\". Journal of Automated Reasoning, Vol. 1, No 4, 1985, 333\u2013376.","journal-title":"Journal of Automated Reasoning"},{"key":"39_CR5","unstructured":"C. Walther: \"A many sorted calculus based on resolution and paramodulation\". Proc. 8th IJCAI, Karlsruhe, W. Germany, August 1983, 882\u2013891."}],"container-title":["Lecture Notes in Computer Science","STACS 88"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0035864","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,9]],"date-time":"2019-02-09T03:08:18Z","timestamp":1549681698000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0035864"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540188346","9783540481904"],"references-count":5,"URL":"https:\/\/doi.org\/10.1007\/bfb0035864","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}