{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T06:04:37Z","timestamp":1726034677971},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030232498"},{"type":"electronic","value":"9783030232504"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-23250-4_16","type":"book-chapter","created":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:01:17Z","timestamp":1562036477000},"page":"227-242","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Inspection and Selection of Representations"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Raggi","sequence":"first","affiliation":[]},{"given":"Aaron","family":"Stockdill","sequence":"additional","affiliation":[]},{"given":"Mateja","family":"Jamnik","sequence":"additional","affiliation":[]},{"given":"Grecia","family":"Garcia Garcia","sequence":"additional","affiliation":[]},{"given":"Holly E. A.","family":"Sutherland","sequence":"additional","affiliation":[]},{"given":"Peter C.-H.","family":"Cheng","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,3]]},"reference":[{"issue":"2\u20133","key":"16_CR1","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/S0360-1315(99)00029-9","volume":"33","author":"S Ainsworth","year":"1999","unstructured":"Ainsworth, S.: The functions of multiple representations. Comput. Educ. 33(2\u20133), 131\u2013152 (1999)","journal-title":"Comput. Educ."},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","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. 5223, pp. 347\u2013349. Springer, Heidelberg (2008). \n                    https:\/\/doi.org\/10.1007\/978-3-540-87730-1_32"},{"issue":"8","key":"16_CR3","doi-asserted-by":"publisher","first-page":"1798","DOI":"10.1109\/TPAMI.2013.50","volume":"35","author":"Y Bengio","year":"2013","unstructured":"Bengio, Y., Courville, A., Vincent, P.: Representation learning: a review and new perspectives. IEEE Trans. Pattern Anal. Mach. Intell. 35(8), 1798\u20131828 (2013)","journal-title":"IEEE Trans. Pattern Anal. Mach. Intell."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Blackwell, A., Green, T.: Notational systems-the cognitive dimensions of notations framework. In: HCI Models, Theories, and Frameworks: Toward an Interdisciplinary Science. Morgan Kaufmann (2003)","DOI":"10.1016\/B978-155860808-5\/50005-8"},{"issue":"2\u20133","key":"16_CR5","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0360-1315(99)00028-7","volume":"33","author":"PC-H Cheng","year":"1999","unstructured":"Cheng, P.C.-H.: Unlocking conceptual learning in mathematics and science with effective representational systems. Comput. Educ. 33(2\u20133), 109\u2013130 (1999)","journal-title":"Comput. Educ."},{"issue":"3","key":"16_CR6","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1111\/j.1756-8765.2009.01065.x","volume":"3","author":"PC-H Cheng","year":"2011","unstructured":"Cheng, P.C.-H.: Probably good diagrams for learning: representational epistemic recodification of probability theory. Top. Cogn. Sci. 3(3), 475\u2013498 (2011)","journal-title":"Top. Cogn. Sci."},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-42333-3_2","volume-title":"Diagrammatic Representation and Inference","author":"PC-H Cheng","year":"2016","unstructured":"Cheng, P.C.-H.: What constitutes an effective representation? In: Jamnik, M., Uesaka, Y., Elzer Schwartz, S. (eds.) Diagrams 2016. LNCS (LNAI), vol. 9781, pp. 17\u201331. Springer, Cham (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-319-42333-3_2"},{"issue":"3","key":"16_CR8","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1109\/TIT.1956.1056813","volume":"2","author":"N Chomsky","year":"1956","unstructured":"Chomsky, N.: Three models for the description of language. IRE Trans. Inf. Theory 2(3), 113\u2013124 (1956)","journal-title":"IRE Trans. Inf. Theory"},{"issue":"2","key":"16_CR9","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/S0019-9958(59)90362-6","volume":"2","author":"N Chomsky","year":"1959","unstructured":"Chomsky, N.: On certain formal properties of grammars. Inf. Control 2(2), 137\u2013167 (1959)","journal-title":"Inf. Control"},{"key":"16_CR10","unstructured":"Coquand, T.: Type theory. In: Stanford Encyclopedia of Philosophy (2006)"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60\u201366. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131\u2013146. Springer, Cham (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-319-03545-1_9"},{"issue":"3","key":"16_CR13","doi-asserted-by":"publisher","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. J. Log. Lang. Inf. 8(3), 297\u2013321 (1999)","journal-title":"J. Log. Lang. Inf."},{"key":"16_CR14","unstructured":"Jupyter. \n                    jupyter.org"},{"key":"16_CR15","unstructured":"Kaufmann, M., Moore, J.S.: ACL2: an industrial strength version of Nqthm. In: Proceedings of 11th Annual Conference on Computer Assurance, COMPASS 1996, pp. 23\u201334. IEEE (1996)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-39634-2_6","volume-title":"Interactive Theorem Proving","author":"D K\u00fchlwein","year":"2013","unstructured":"K\u00fchlwein, D., Blanchette, J.C., Kaliszyk, C., Urban, J.: MaSh: machine learning for sledgehammer. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 35\u201350. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-39634-2_6"},{"key":"16_CR18","unstructured":"Matlab. \n                    mathworks.com"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 4424, pp. 519\u2013522. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-71209-1_40"},{"key":"16_CR20","volume-title":"Human Problem Solving","author":"A Newell","year":"1972","unstructured":"Newell, A.: Human Problem Solving. Prentice-Hall Inc., Upper Saddle River (1972)"},{"key":"16_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, Heidelberg (2002). \n                    https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"16_CR22","unstructured":"GNU Octave. \n                    octave.org"},{"issue":"4","key":"16_CR23","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s11786-016-0275-z","volume":"10","author":"D Raggi","year":"2016","unstructured":"Raggi, D., Bundy, A., Grov, G., Pease, A.: Automating change of representation for proofs in discrete mathematics (extended version). Math. Comput. Sci. 10(4), 429\u2013457 (2016)","journal-title":"Math. Comput. Sci."},{"key":"16_CR24","unstructured":"SageMath. \n                    sagemath.org"},{"issue":"2","key":"16_CR25","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10849-017-9250-6","volume":"26","author":"G Stapleton","year":"2017","unstructured":"Stapleton, G., Jamnik, M., Shimojima, A.: What makes an effective representation of information: a formal account of observational advantages. J. Log. Lang. Inf. 26(2), 143\u2013177 (2017)","journal-title":"J. Log. Lang. Inf."},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-662-44043-8_28","volume-title":"Diagrammatic Representation and Inference","author":"M Urbas","year":"2014","unstructured":"Urbas, M., Jamnik, M.: A framework for heterogeneous reasoning in formal and informal domains. In: Dwyer, T., Purchase, H., Delaney, A. (eds.) Diagrams 2014. LNCS (LNAI), vol. 8578, pp. 277\u2013292. Springer, Heidelberg (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-662-44043-8_28"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","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. 7352, pp. 163\u2013177. Springer, Heidelberg (2012). \n                    https:\/\/doi.org\/10.1007\/978-3-642-31223-6_19"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-540-25984-8_24","volume-title":"Automated Reasoning","author":"D Winterstein","year":"2004","unstructured":"Winterstein, D., Bundy, A., Gurr, C.: Dr.Doodle: a diagrammatic theorem prover. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 331\u2013335. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-25984-8_24"},{"key":"16_CR29","unstructured":"WordNet (2010). \n                    wordnet.princeton.edu"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-23250-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:07:05Z","timestamp":1562036825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-23250-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030232498","9783030232504"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-23250-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2019\/cicm.php?event=&menu=general","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}