{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:11:10Z","timestamp":1746115870825,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642451133"},{"type":"electronic","value":"9783642451140"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45114-0_2","type":"book-chapter","created":{"date-parts":[[2013,11,22]],"date-time":"2013-11-22T05:10:42Z","timestamp":1385097042000},"page":"12-23","source":"Crossref","is-referenced-by-count":0,"title":["The Inverse Method for Many-Valued Logics"],"prefix":"10.1007","author":[{"given":"Laura","family":"Kov\u00e1cs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Mantsivoda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-540-72788-0_4","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C. Ans\u00f3tegui","year":"2007","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J., Many\u00e0, F.: Mapping CSP into Many-Valued SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 10\u201315. Springer, Heidelberg (2007)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/BFb0013053","volume-title":"Logic Programming and Automated Reasoning","author":"M. Baaz","year":"1992","unstructured":"Baaz, M., Ferm\u00fcller, C.G.: Resolution for many-valued logics. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 107\u2013118. Springer, Heidelberg (1992)"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1006\/jsco.1995.1021","volume":"19","author":"M. Baaz","year":"1995","unstructured":"Baaz, M., Ferm\u00fcller, C.G.: Resolution-based theorem proving for many-valued logics. Journal of Symbolic Computations\u00a019, 353\u2013391 (1995)","journal-title":"Journal of Symbolic Computations"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/3-540-56944-8_66","volume-title":"Logic Programming and Automated Reasoning","author":"M. Baaz","year":"1993","unstructured":"Baaz, M., Ferm\u00fcller, C.G., Ovrutcki, A., Zach, R.: MULTLOG: a system for axiomatizing many-valued logics. In: Voronkov, A. (ed.) LPAR 1993. LNCS, vol.\u00a0698, pp. 345\u2013347. Springer, Heidelberg (1993)"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Baaz, M., Ferm\u00fcller, C.G., Zach, R.: Systematic construction of natural deduction systems for many-valued logics. In: Proc. 23rd International Symposium on Multiple-Valued Logics, Los Gatos, CA, pp. 208\u2013213. IEEE Computer Society Press (1993)","DOI":"10.1109\/ISMVL.1993.289558"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 2, vol.\u00a0I, pp. 19\u201399. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Many\u00e0, F.: Transformations between signed and classical clause logic. In: ISMVL, pp. 248\u2013255 (1999)","DOI":"10.1109\/ISMVL.1999.779724"},{"issue":"2","key":"2_CR8","doi-asserted-by":"publisher","first-page":"473","DOI":"10.2307\/2274395","volume":"52","author":"W.A. Carnielli","year":"1987","unstructured":"Carnielli, W.A.: Systematization of finite many-valued logics through the method of tableaux. Journal of Symbolic Logic\u00a052(2), 473\u2013493 (1987)","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"2_CR9","first-page":"59","volume":"8","author":"W.A. Carnielli","year":"1991","unstructured":"Carnielli, W.A.: On sequents and tableaux for many-valued logics. Journal of Non-Classical Logics\u00a08(1), 59\u201376 (1991)","journal-title":"Journal of Non-Classical Logics"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: The inverse method. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 4, vol.\u00a0I, pp. 179\u2013272. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50006-0"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 9, vol.\u00a0I, pp. 535\u2013610. Elsevier Science (2001)","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"key":"2_CR12","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematical Zeitschrift\u00a039, 176\u2013210, 405\u2013431 (1934); Translated as [13]","journal-title":"Mathematical Zeitschrift"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68\u2013131. North Holland, Amsterdam (1969); reprinted from [12]","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"2_CR14","volume-title":"Automated Deduction in Multiple-Valued Logics","author":"R. H\u00e4hnle","year":"1993","unstructured":"H\u00e4hnle, R.: Automated Deduction in Multiple-Valued Logics. Clarendon Press, Oxford (1993)"},{"issue":"6","key":"2_CR15","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1093\/logcom\/4.6.905","volume":"4","author":"R. H\u00e4hnle","year":"1994","unstructured":"H\u00e4hnle, R.: Short conjunctive normal forms in finitely valued logics. Journal of Logic and Computation\u00a04(6), 905\u2013927 (1994)","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"2_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00245018","volume":"5","author":"V. Lifschitz","year":"1989","unstructured":"Lifschitz, V.: What is the inverse method? Journal of Automated Reasoning\u00a05(1), 1\u201323 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR17","unstructured":"Yu, S.: Maslov. An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus. Soviet Mathematical Doklady\u00a0172(1), 22\u201325 (1983); reprinted as [20]"},{"key":"2_CR18","unstructured":"Maslov, S.Y.: Relationship between tactics of the inverse method and the resolution method. Zapiski Nauchnyh Seminarov LOMI\u00a016 (1969) (in Russian); Reprinted as [21]"},{"key":"2_CR19","unstructured":"Maslov, S.Y.: Proof-search strategies for methods of the resolution type. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol.\u00a06, pp. 77\u201390. American Elsevier (1971)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Maslov, S.Y.: An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning (Classical papers on Computational Logic), vol.\u00a02, pp. 48\u201354. Springer (1983); reprinted from [17]","DOI":"10.1007\/978-3-642-81955-1_3"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Yu Maslov, S.: Relationship between tactics of the inverse method and the resolution method. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning (Classical papers on Computational Logic), vol.\u00a02, pp. 264\u2013272. Springer (1983); Reprinted from [18]","DOI":"10.1007\/978-3-642-81955-1_16"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-02959-2_19","volume-title":"Automated Deduction \u2013 CADE-22","author":"S. McLaughlin","year":"2009","unstructured":"McLaughlin, S., Pfenning, F.: Efficient intuitionistic theorem proving with the polarized inverse method. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 230\u2013244. Springer, Heidelberg (2009)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/3-540-52335-9_55","volume-title":"COLOG-88","author":"G. Mints","year":"1990","unstructured":"Mints, G.: Gentzen-type systems and resolution rules. Part I. Propositional logic. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, pp. 198\u2013231. Springer, Heidelberg (1990)"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Murray, N.V., Rosenthal, E.: Improving tableau deductions in multiple-valued logics. In: Proceedings of the 21st International Symposium on Multiple-Valued logics, Los Alamitos, pp. 230\u2013237. IEEE Computer Society Press (1991)","DOI":"10.1109\/ISMVL.1991.130735"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Murray, N.V., Rosenthal, E.: Resolution and path dissolution in multiple-valued logics. In: Proceedings International Symposium on Methodologies for Intelligent Systems, Charlotte (1991)","DOI":"10.1007\/3-540-54563-8_120"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-56804-2_26","volume-title":"Methodologies for Intelligent Systems","author":"N.V. Murray","year":"1993","unstructured":"Murray, N.V., Rosenthal, E.: Signed formulas: a liftable meta-logic for multiple-valued logics. In: Komorowski, J., Ra\u015b, Z.W. (eds.) ISMIS 1993. LNCS, vol.\u00a0689, pp. 230\u2013237. Springer, Heidelberg (1993)"},{"key":"2_CR27","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/S0747-7171(10)80002-1","volume":"13","author":"P. O\u2019Hearn","year":"1992","unstructured":"O\u2019Hearn, P., Stachniak, Z.: A resolution framework for finitely-valued first-order logics. Journal of Symbolic Computations\u00a013, 235\u2013254 (1992)","journal-title":"Journal of Symbolic Computations"},{"key":"2_CR28","unstructured":"Robinson, J.A.: Robinson. Automatic deduction with hyper-resolution. International Journal of Computer Mathematics\u00a01, 227\u2013234 (1965); Reprinted as [29]"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Robinson, J.A.: Automatic deduction with hyperresolution. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning. Classical Papers on Computational Logic, vol.\u00a01, pp. 416\u2013423. Springer (1983); Originally appeared as [28]","DOI":"10.1007\/978-3-642-81952-0_27"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Rousseau, G.: Sequents in many-valued logic 1. Fundamenta Mathematikae, LX, 23\u201333 (1967)","DOI":"10.4064\/fm-60-1-23-33"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/3-540-52885-7_138","volume-title":"10th International Conference on Automated Deduction","author":"A. Voronkov","year":"1990","unstructured":"Voronkov, A.: LISS \u2014 the logic inference search system. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 677\u2013678. Springer, Heidelberg (1990)"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"648","DOI":"10.1007\/3-540-55602-8_198","volume-title":"Automated Deduction - CADE-11","author":"A. Voronkov","year":"1992","unstructured":"Voronkov, A.: Theorem proving in non-standard logics based on the inverse method. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 648\u2013662. Springer, Heidelberg (1992)"},{"key":"2_CR33","unstructured":"Voronkov, A.: Deciding K using kk. In: Cohn, A.G., Giunchiglia, F., Selman, B. (eds.) Principles of Knowledge Representation and Reasoning (KR 2000), pp. 198\u2013209 (2000)"},{"issue":"2","key":"2_CR34","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1145\/371316.371511","volume":"2","author":"A. Voronkov","year":"2001","unstructured":"Voronkov, A.: How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. ACM Transactions on Computational Logic\u00a02(2), 182\u2013215 (2001)","journal-title":"ACM Transactions on Computational Logic"}],"container-title":["Lecture Notes in Computer Science","Advances in Artificial Intelligence and Its Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-45114-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T22:48:27Z","timestamp":1746053307000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45114-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642451133","9783642451140"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45114-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}