{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:57:56Z","timestamp":1725663476910},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_179","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:20:06Z","timestamp":1330251606000},"page":"385-399","source":"Crossref","is-referenced-by-count":1,"title":["Semantic entailment in non classical logics based on proofs found in classical logic"],"prefix":"10.1007","author":[{"given":"Ricardo","family":"Caferra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Demri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0890-5401(91)90023-U","volume":"92","author":"A. Avron","year":"1991","unstructured":"A. Avron. Simple Consequence Relations. Information and Computation, 92:105\u2013139, 1991.","journal-title":"Information and Computation"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"T. Boy de la Tour, R. Caferra, and G. Chaminade. Some tools for an Inference Laboratory (ATINF). In CADE-9, pages 744\u2013745. Springer-Verlag, LNCS 310, 1988.","DOI":"10.1007\/BFb0012877"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"R. Caferra and S. Demri. Semantic entailment in non classical logics based on proofs found in classical logic, 1992. Extended version to appear.","DOI":"10.1007\/3-540-55602-8_179"},{"key":"29_CR4","unstructured":"R. Caferra, S. Demri, and M. Herment. Logic morphisms as a framework for the backward transfer of lemmas and strategies in some modal and epistemic logics. In AAAI-9, pages 421\u2013426. AAAI, MIT Press, July 1991."},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"R. Caferra, M. Herment, and N. Zabel. User-oriented theorem proving with the ATINF graphic proof editor. In FAIR' 91, pages 2\u201310. Springer-Verlag, LNAI 535, 1991.","DOI":"10.1007\/3-540-54507-7_1"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"H. D. Ebbinghaus. Extended logics: the general framework. In J. Barwise and Feferman S., editors, Model theoretic logics, pages 25\u201376. Springer-Verlag, 1985.","DOI":"10.1017\/9781316717158.005"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"M. C. Fitting. Proof methods for modal and intuitionistic logics. D. Reidel Publishing Co., 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"29_CR8","volume-title":"PhD thesis","author":"A. Herzig","year":"1989","unstructured":"A. Herzig. Raisonnement automatique en logique modale et algorithmes d'unification. PhD thesis, Universit\u00e9 Paul Sabatier, Toulouse, July 1989."},{"key":"29_CR9","unstructured":"K. Konolige. A deduction model of belief. Pitman, 1986."},{"key":"29_CR10","first-page":"380","volume":"39","author":"C.R. Mann","year":"1974","unstructured":"C.R. Mann. Equivalence of deduction in proof theory and free cartesian closed categories. Journal of Symbolic Logic, 39:380\u2013381, 1974.","journal-title":"Journal of Symbolic Logic"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"J. Meseguer. General logic. In H-D Ebbinghaus, editor, Logic Colloquium '87, pages 275\u2013330. North-Holland, 1987.","DOI":"10.1016\/S0049-237X(08)70132-0"},{"issue":"8","key":"29_CR12","doi-asserted-by":"crossref","first-page":"852","DOI":"10.1109\/TC.1976.1674704","volume":"25","author":"C. Morgan","year":"1976","unstructured":"C. Morgan. Methods for automated theorem proving in non classical logics. IEEE Transactions on Computers, 25(8):852\u2013862, August 1976.","journal-title":"IEEE Transactions on Computers"},{"key":"29_CR13","unstructured":"H.J. Ohlbach. A resolution calculus for modal logics. PhD thesis, FB Informatik Univ. of Kaiserslautern, 1988."},{"key":"29_CR14","unstructured":"H.J. Ohlbach. Context Logic. Technical report, FB Informatik Univ. of Kaiserlautern, 1989."},{"key":"29_CR15","first-page":"253","volume":"3","author":"E. Orlowska","year":"1979","unstructured":"E. Orlowska. Resolution systems and their applications I. Fundamenta Informaticae, 3:253\u2013268, 1979.","journal-title":"Fundamenta Informaticae"},{"key":"29_CR16","doi-asserted-by":"crossref","first-page":"333","DOI":"10.3233\/FI-1980-3306","volume":"3","author":"E. Orlowska","year":"1980","unstructured":"E. Orlowska. Resolution systems and their applications II. Fundamenta Informaticae, 3:333\u2013362, 1980.","journal-title":"Fundamenta Informaticae"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"D. Scott. Completeness and axiomatizability in many-valued logic. In L. Henkin et al., editor, Tarski Symposium, pages 411\u201335, 1974.","DOI":"10.1090\/pspum\/025\/0363802"}],"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_179.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T04:27:40Z","timestamp":1640924860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_179"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_179","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}