{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T12:59:12Z","timestamp":1790686752552,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540556022","type":"print"},{"value":"9783540472520","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_198","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T05:21:40Z","timestamp":1330233700000},"page":"648-662","source":"Crossref","is-referenced-by-count":13,"title":["Theorem proving in non-standard logics based on the inverse method"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Voronkov","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"48_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00302639","volume":"6","author":"I. Auffray","year":"1990","unstructured":"I. Auffray, P. Enjalbert, and J-J. Hebrard. Strategies for modal resolution: Results and problems. Journal of Automated Reasoning, 6:1\u201338, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"48_CR2","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated theorem proving. Vieweg Verlag, 1982.","DOI":"10.1007\/978-3-322-90100-2"},{"key":"48_CR3","unstructured":"J-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989."},{"issue":"1","key":"48_CR4","first-page":"47","volume":"45","author":"V.N. Grishin","year":"1981","unstructured":"V.N. Grishin. Predicate and set-theoretic calculi based on logic without the contraction rule (in Russian). Izvestiya Akad. Nauk SSSR, 45(1):47\u201368, 1981.","journal-title":"Izvestiya Akad. Nauk SSSR"},{"issue":"3","key":"48_CR5","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0304-3975(84)90047-1","volume":"32","author":"J. Ketonen","year":"1984","unstructured":"J. Ketonen and R. Weyhrauch. A decidable fragment of predicate calculus. Theoretical Computer Science, 32(3):297\u2013309, 1984.","journal-title":"Theoretical Computer Science"},{"key":"48_CR6","unstructured":"S.C. Kleene. Permutability of inferences in Gentzen's calculi LK and LJ. Memoirs of the American Mathematical Society, 10, 1952."},{"issue":"1","key":"48_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00883928","volume":"5","author":"V. Lifschitz","year":"1986","unstructured":"V. Lifschitz. What is the inverse method? Journal of Automated Reasoning, 5(1):1\u201324, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"48_CR8","doi-asserted-by":"crossref","unstructured":"S.Yu. Maslov. An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus. In J.Siekmann and G.Wrightson, editors, Automation of Reasoning (Classical papers on Computational Logic), volume 2, pages 48\u201354. Springer Verlag, 1983.","DOI":"10.1007\/978-3-642-81955-1_3"},{"key":"48_CR9","doi-asserted-by":"crossref","unstructured":"S.Yu. Maslov. Relationship between tactics of the inverse method and the resolution method. In J.Siekmann and G.Wrightson, editors, Automation of Reasoning (Classical papers on Computational Logic), volume 2, pages 264\u2013272. Springer Verlag, 1983.","DOI":"10.1007\/978-3-642-81955-1_16"},{"key":"48_CR10","unstructured":"S.Yu. Maslov. Theory of Deductive Systems and its Applications. MIT Press, 1987."},{"key":"48_CR11","unstructured":"D. Mey. Private communications."},{"key":"48_CR12","doi-asserted-by":"crossref","unstructured":"G. Mints. Gentzen-type systems and resolution rules. Part I. Propositional logic. In P. Martin-L\u00f6f and G. Mints, editors, COLOG-88, volume 417 of Lecture Notes in Computer Science, pages 198\u2013231. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52335-9_55"},{"key":"48_CR13","unstructured":"H.-Y\u00fc. Ohlbach and A. Herzig. Parameter structures for parameterized modal operators. In Proc. IJCAP'91, pages 512\u2013517, 1991."},{"key":"48_CR14","doi-asserted-by":"crossref","unstructured":"N. Shankar. Proof search in the intuitionistic sequent calculus. In 12th International Conference on Automated Deduction, Lecture Notes in Computer Science, 1992.","DOI":"10.1007\/3-540-55602-8_189"},{"key":"48_CR15","first-page":"677","volume-title":"volume 449 of Lecture Notes in Computer Science","author":"A.A. Voronkov","year":"1990","unstructured":"A.A. Voronkov. LISS \u2014 the logic inference search system. In Mark Stickel, editor, Proc. Int. Conf. on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 677\u2013678, Kaiserslautern, Germany, 1990. Springer Verlag."},{"key":"48_CR16","doi-asserted-by":"crossref","unstructured":"A.A. Voronkov. A proof-search method for the first order logic. In P.Martin-Lof and G.Mintz, editors, COLOG'88, volume 417 of Lecture Notes in Computer Science, pages 327\u2013340. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52335-9_63"},{"key":"48_CR17","unstructured":"L.A. Wallen. Automated Deduction in Nonclassical Logics. MIT Press, 1990."},{"issue":"2","key":"48_CR18","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/0168-0072(89)90053-5","volume":"42","author":"N.K. Zamov","year":"1989","unstructured":"N.K. Zamov. Maslov's inverse method and decidable classes. Annals of Pure and Applied Logic, 42(2):165\u2013194, 1989.","journal-title":"Annals of Pure and Applied Logic"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_198.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:00:25Z","timestamp":1605628825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_198"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_198","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992]]}}}