{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,31]],"date-time":"2025-07-31T00:25:32Z","timestamp":1753921532472},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055151","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"443-460","source":"Crossref","is-referenced-by-count":4,"title":["Mechanizing relevant logics with HOL"],"prefix":"10.1007","author":[{"given":"Hajime","family":"Sawamura","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daisaku","family":"Asanuma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"26_CR1","unstructured":"A. R. Anderson and N. D. Belnap, Jr. Entailment: The Logic of Relevance and Necessity, Vol. 1, Princeton Univ. Press, 1975."},{"key":"26_CR2","unstructured":"D. Basin, S. Matthews, and L. Vigano. Natural Deduction for Non-Classical Logics, to appear in Studia Logica, 1998."},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"J. M. Dunn. Relevance Logic and Entailment. In D. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, Vol. III, D. Reidel Publishing Company, pages 117\u2013224, 1986.","DOI":"10.1007\/978-94-009-5203-4_3"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"D. M. Gabbay. LDS \u2014 Labelled Deductive Systems (Volume 1 \u2014 Foundations), Clarendon Press, 1996.","DOI":"10.1093\/oso\/9780198538332.003.0001"},{"key":"26_CR5","unstructured":"M. J. C. Gordon. and T. F. Melham. Introduction to HOL, Cambridge University Press, 1993."},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"P. de Groote. Linear Logic with Isabelle: Pruning the Proof Search Tree, LNAI 918, Springer, pages 263\u2013277, 1995.","DOI":"10.1007\/3-540-59338-1_41"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"H. J. Ohlbach and G. Wrightson. Solving a Problem in Relevance Logic with an Automated Theorem Prover, LNCS 170, Springer, pages 496\u2013508, 1984.","DOI":"10.1007\/978-0-387-34768-4_29"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"L. Paulson. Isabelle, a Generic Theorem Prover, LNCS 828, Springer, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"26_CR9","unstructured":"S. Read. Relevant Logic, Basil Blackwell, 1988."},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"R. Routley and R. Meyer. The Semantics of Entailment, In Leblanc (ed.), Truth, Syntax and Modality, North-Holland, pages 199\u2013243, 1972.","DOI":"10.1016\/S0049-237X(08)71541-6"},{"key":"26_CR11","unstructured":"P. B. Thistlewaite, M. A. McRobbie, and R. K. Meyer. Automated Theorem-Proving in Non-Classical Logics, Pitman Publishing, 1988."},{"key":"26_CR12","unstructured":"H. Sawamura, T. Minami, K. Yokota, and K. Ohashi. A logic programming approach to specifying logics and constructing proofs, Proc. of the Seventh International Conference on Logic Programming, The MIT Press, pages 405\u2013424, 1990."},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"H. Sawamura, T. Minami, and T. Ohtani. EUODHILOS: A general reasoning system for a variety of logics, LNAI 624, Springer, pages 501\u2013503, 1992.","DOI":"10.1007\/BFb0013101"},{"key":"26_CR14","first-page":"1059","volume":"49","author":"A. Urquhart","year":"1984","unstructured":"A. Urquhart. The undecidability of entailment and relevant implication, JSL, 49:1059\u20131073, 1984.","journal-title":"JSL"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055151","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,5]],"date-time":"2024-02-05T15:54:28Z","timestamp":1707148468000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055151"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0055151","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}