{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:55:15Z","timestamp":1760043315567,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662440421"},{"type":"electronic","value":"9783662440438"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-662-44043-8_28","type":"book-chapter","created":{"date-parts":[[2014,7,23]],"date-time":"2014-07-23T09:49:14Z","timestamp":1406108954000},"page":"277-292","source":"Crossref","is-referenced-by-count":13,"title":["A Framework for Heterogeneous Reasoning in Formal and Informal Domains"],"prefix":"10.1007","author":[{"given":"Matej","family":"Urbas","sequence":"first","affiliation":[]},{"given":"Mateja","family":"Jamnik","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/978-3-540-87730-1_32","volume-title":"Diagrammatic Representation and Inference","author":"D. Barker-Plummer","year":"2008","unstructured":"Barker-Plummer, D., Etchemendy, J., Liu, A., Murray, M., Swoboda, N.: Openproof - A flexible framework for heterogeneous reasoning. In: Stapleton, G., Howse, J., Lee, J. (eds.) Diagrams 2008. LNCS (LNAI), vol.\u00a05223, pp. 347\u2013349. Springer, Heidelberg (2008)"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/978-3-642-14203-1_9","volume-title":"Automated Reasoning","author":"S. B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Nipkow, T.: Sledgehammer: Judgement day. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 107\u2013121. Springer, Heidelberg (2010)"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Gardner, P., Zarfaty, U.: Context logic as modal logic: completeness and parametric inexpressivity. In: POPL, pp. 123\u2013134. ACM (2007)","DOI":"10.1145\/1190216.1190236"},{"key":"28_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/978-3-540-73086-6_6","volume-title":"Towards Mechanized Mathematical Assistants","author":"W.M. Farmer","year":"2007","unstructured":"Farmer, W.M.: Biform Theories in Chiron. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 66\u201379. Springer, Heidelberg (2007)"},{"issue":"1","key":"28_CR5","first-page":"29","volume":"65","author":"F. Giunchiglia","year":"1994","unstructured":"Giunchiglia, F., Serafini, L.: Multilanguage hierarchical logics, or: How we can do without modal logics. AI\u00a065(1), 29\u201370 (1994)","journal-title":"AI"},{"key":"28_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/3-540-45620-1_12","volume-title":"Automated Deduction - CADE-18","author":"J.H. Siekmann","year":"2002","unstructured":"Siekmann, J.H., et al.: Proof development with \u03a9MEGA. In: Voronkov, A. (ed.) CADE-18. LNCS (LNAI), vol.\u00a02392, pp. 144\u2013149. Springer, Heidelberg (2002)"},{"issue":"3","key":"28_CR7","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1023\/A:1008323427489","volume":"8","author":"M. Jamnik","year":"1999","unstructured":"Jamnik, M., Bundy, A., Green, I.: On Automating Diagrammatic Proofs of Arithmetic Arguments. JOLLI\u00a08(3), 297\u2013321 (1999)","journal-title":"JOLLI"},{"key":"28_CR8","unstructured":"Kortenkamp, U., Richter-Gebert, J.: Using automatic theorem proving to improve the usability of geometry software. In: Procedings of the Mathematical User-Interfaces Workshop, pp. 1\u201312 (2004)"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/978-3-540-71209-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Mossakowski","year":"2007","unstructured":"Mossakowski, T., Maeder, C., L\u00fcttich, K.: The Heterogeneous Tool Set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 519\u2013522. Springer, Heidelberg (2007)"},{"key":"28_CR10","unstructured":"Paulson, L.C.: Isabelle - A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"issue":"1","key":"28_CR11","first-page":"86","volume":"10","author":"S.J. Shin","year":"2004","unstructured":"Shin, S.J.: Heterogeneous Reasoning and its Logic. BSL\u00a010(1), 86\u2013106 (2004)","journal-title":"BSL"},{"key":"28_CR12","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1007\/978-3-642-31365-3_44","volume-title":"Automated Reasoning","author":"M. Urbas","year":"2012","unstructured":"Urbas, M., Jamnik, M.: Diabelli: A heterogeneous proof system. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol.\u00a07364, pp. 559\u2013566. Springer, Heidelberg (2012)"},{"key":"28_CR13","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/978-3-642-31223-6_19","volume-title":"Diagrammatic Representation and Inference","author":"M. Urbas","year":"2012","unstructured":"Urbas, M., Jamnik, M., Stapleton, G., Flower, J.: Speedith: A diagrammatic reasoner for spider diagrams. In: Cox, P., Plimmer, B., Rodgers, P. (eds.) Diagrams 2012. LNCS (LNAI), vol.\u00a07352, pp. 163\u2013177. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Diagrammatic Representation and Inference"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44043-8_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T21:18:53Z","timestamp":1743801533000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-44043-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662440421","9783662440438"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44043-8_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}