{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:26Z","timestamp":1725663686243},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540523352"},{"type":"electronic","value":"9783540469636"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52335-9_63","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:31:16Z","timestamp":1330205476000},"page":"327-338","source":"Crossref","is-referenced-by-count":5,"title":["A proof-search method for the first order logic"],"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,8]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"2","author":"P.B. Andrews","year":"1981","unstructured":"Andrews P.B.: Theorem proving via general matings. J.Assoc. Comp. Math. 2(1981), v.28, 193\u2013214","journal-title":"J.Assoc. Comp. Math."},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Bibel W.: Automated theorem proving. Vieweg Verlag, (1982)","DOI":"10.1007\/978-3-322-90100-2"},{"key":"21_CR3","unstructured":"de Champeaux D.: Sub-problem finder and instance checker: two cooperating preprocessors for theorem-provers. 6th IJCAI, (1981), v.1, 191\u2013196"},{"key":"21_CR4","unstructured":"Chang C., Lee R.C.: Symbolic logic and mechanical theorem proving. Academic Press, (1973)"},{"key":"21_CR5","unstructured":"Dragalin A.: A proof-search method. Proc. 8th Int. Congress on Logic, Methodology and Philosophy of Sci. Moscow, (1987)"},{"key":"21_CR6","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen G.: Untersuchungen uber das logishe Schliessen. Math. Z. (1935), v.39, 176\u2013210; 405\u2013431","journal-title":"Math. Z."},{"key":"21_CR7","unstructured":"Loveland D.: Automated theorem proving: a logical basis. North Holland, (1978)"},{"key":"21_CR8","unstructured":"Maslov S.Y.: Inverse method of establishing deducibility for logical calculi. Trudy Math. Inst. (1968), v.98"},{"key":"21_CR9","unstructured":"Schutte K.: Beweistheorie. Springer Verlag, (1960)"},{"key":"21_CR10","unstructured":"Stickel M.: A Prolog technology theorem prover. 8th International Conf. on Automated Deduction, Lecture Notes in Comput. Sci. (1986), v.230"},{"key":"21_CR11","first-page":"109","volume":"107","author":"A.A. Voronkov","year":"1985","unstructured":"Voronkov A.A.: A proof search method. Vychislitelnye sistemy, Novosibirsk, (1985), v.107, 109\u2013124 (in Russian)","journal-title":"Vychislitelnye sistemy, Novosibirsk"},{"key":"21_CR12","unstructured":"Voronkov, A.A.: Degtjarev A.I.: Automated theorem proving I, II. Kibernetika, (1986), v.3, (1987) v.4 (In Russian)"}],"container-title":["Lecture Notes in Computer Science","COLOG-88"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52335-9_63.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:07:44Z","timestamp":1619572064000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52335-9_63"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540523352","9783540469636"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-52335-9_63","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}