{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:55:41Z","timestamp":1725663341690},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540528852"},{"type":"electronic","value":"9783540471714"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52885-7_138","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:47:21Z","timestamp":1330206441000},"page":"677-678","source":"Crossref","is-referenced-by-count":3,"title":["Liss \u2014 The logic inference search system"],"prefix":"10.1007","author":[{"given":"A. A.","family":"Voronkov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"64_CR1","unstructured":"Ono H. Semantic analysis of the logics without structure rules, Studia Logica, 1986."},{"key":"64_CR2","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(84)90047-1","volume":"32","author":"J. Ketonen","year":"1984","unstructured":"Ketonen J., Weyhrauch R. A decidable fragment of predicate calculus, Theoretical Computer Science 32, 1984, pp. 297\u2013307.","journal-title":"Theoretical Computer Science"},{"key":"64_CR3","doi-asserted-by":"crossref","unstructured":"Mey D. A predicate calculus with control of derivations, to be published in Proc. 3rd Computer Science Logic Workshop, LNCS, 1990.","DOI":"10.1007\/3-540-52753-2_44"},{"key":"64_CR4","unstructured":"Maslov S.Y. The inverse method of establishing deducibility for logical calculi, Trudy Instituta Matematiki, vol. 67, 1968."},{"key":"64_CR5","unstructured":"Voronkov A.A. A proof-search method for first-order logic. \u2014 In: COLOG-88 (papers presented at the Int. Conf. on Computer Logic), Part 2, Tallinn, 1988, p.104\u2013118. (Also to be published in LNCS)."},{"key":"64_CR6","first-page":"1","volume":"138","author":"L. Wos","year":"1982","unstructured":"Wos L. Solving open questions with an automated theorem proving program, Proc. 6th CADE, LNCS 138, 1982, pp. 1\u201331.","journal-title":"LNCS"},{"key":"64_CR7","first-page":"70","volume":"138","author":"E.L. Lusk","year":"1982","unstructured":"Lusk E.L., McCune W.W., Overbeek R.A. Logic Machine Architecture: kernel functions, Proc. 6th CADE, LNCS 138, 1982, pp. 70\u201384.","journal-title":"LNCS"},{"key":"64_CR8","unstructured":"McCune W.W. OTTER user's guide, Argonne National Laboratory, December, 1988."},{"issue":"4","key":"64_CR9","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/BF02737109","volume":"25","author":"U.R. Schmerl","year":"1988","unstructured":"Schmerl U.R. Resolution on formula trees. \u2014 Acta Informatica, 25(4), 1988, 425\u2013438.","journal-title":"Acta Informatica"}],"container-title":["Lecture Notes in Computer Science","10th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52885-7_138.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:34Z","timestamp":1605648334000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52885-7_138"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540528852","9783540471714"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-52885-7_138","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}