{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:28Z","timestamp":1725488608858},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540671909"},{"type":"electronic","value":"9783540465089"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_11","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:02:03Z","timestamp":1186171323000},"page":"167-174","source":"Crossref","is-referenced-by-count":0,"title":["Implicational Completeness of Signed Resolution"],"prefix":"10.1007","author":[{"given":"Christian G.","family":"Ferm\u00fcller","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"11_CR1","unstructured":"M. Baaz. Automatisches Beweisen f\u00fcr endlichwertige Logiken. In Jahrbuch 1989 der Kurt G\u00f6del-Gesellschaft, pages 105\u2013107. Kurt G\u00f6del Society, 1989."},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1006\/jsco.1995.1021","volume":"19","author":"M. Baaz","year":"1995","unstructured":"M. Baaz and C. G. Ferm\u00fcller. Resolution-based theorem proving for many-valued logics. J. Symbolic Computation, 19:353\u2013391, 1995.","journal-title":"J. Symbolic Computation"},{"key":"11_CR3","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"M.S. Garey","year":"1979","unstructured":"M.S. Garey and D.S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, San Francisco, 1979."},{"issue":"2","key":"11_CR4","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1145\/3149.214118","volume":"32","author":"G. Gottlob","year":"1985","unstructured":"G. Gottlob and A. Leitsch. On the efficiency of subsumbtion algorithms. Journal of the ACM, 32(2):280\u2013295, 1985.","journal-title":"Journal of the ACM"},{"key":"11_CR5","volume-title":"Automated Deduction in Multiple-valued Logics","author":"R. H\u00e4hnle","year":"1993","unstructured":"R. H\u00e4hnle. Automated Deduction in Multiple-valued Logics. Clarendon Press, Oxford, 1993."},{"issue":"6","key":"11_CR6","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1093\/logcom\/4.6.905","volume":"4","author":"R. H\u00e4hnle","year":"1994","unstructured":"R. H\u00e4hnle. Short conjunctive normal forms in finitely-valued logics. Journal of Logic and Computation, 4(6):905\u2013927, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"11_CR7","volume-title":"A completeness theorem and a computer program for finding theorems derivable from given axioms","author":"R.C.T. Lee","year":"1967","unstructured":"R.C.T. Lee. A completeness theorem and a computer program for finding theorems derivable from given axioms. Ph.D. Thesis, University of California, Berkely, 1967."},{"key":"11_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60605-2","volume-title":"The Resolution Calculus","author":"A. Leitsch","year":"1997","unstructured":"A. Leitsch. The Resolution Calculus. Springer, Berlin, Heidelberg, New York, 1997."},{"key":"11_CR9","series-title":"Lect Notes Comput Sci","volume-title":"13th Int. Conf. on Automated Deduction (CADE\u201996)","author":"G. Salzer","year":"1996","unstructured":"G. Salzer. Optimal axiomatizations for multiple-valued operators and quantifiers based on semi-lattices. In 13th Int. Conf. on Automated Deduction (CADE\u201996), LNCS (LNAI). Springer, 1996."},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0304-3975(88)90146-6","volume":"59","author":"M. Schmidt-Schauss","year":"1988","unstructured":"M. Schmidt-Schauss. Implication of clauses is undecidable. Theoretical Computer Science, 59:287\u2013296, 1988.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Classical and Non-Classical Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46508-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T22:50:27Z","timestamp":1550443827000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}