{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:31Z","timestamp":1725456211438},"publisher-location":"Berlin, Heidelberg","reference-count":6,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540193432"},{"type":"electronic","value":"9783540392163"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/bfb0012877","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"744-745","source":"Crossref","is-referenced-by-count":7,"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,9]]},"reference":[{"key":"58_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":"58_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":"58_CR3","unstructured":"M. Schmidt-Schauss: \"A many-Sorted calculus with polymorphic functions based on resolution and paramodulation\". Interner Bericht. Fachbereich Informatik. Universitat Kaiserslautern."},{"key":"58_CR4","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":"58_CR5","doi-asserted-by":"publisher","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":"58_CR6","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","9th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012877","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,21]],"date-time":"2019-01-21T13:53:44Z","timestamp":1548078824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012877"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540193432","9783540392163"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/bfb0012877","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}