{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T21:19:38Z","timestamp":1773350378050,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":62,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,8,14]],"date-time":"2017-08-14T00:00:00Z","timestamp":1502668800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,8,14]]},"DOI":"10.1145\/3105726.3106184","type":"proceedings-article","created":{"date-parts":[[2017,8,15]],"date-time":"2017-08-15T12:25:25Z","timestamp":1502799925000},"page":"83-92","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Theorem Provers as a Learning Tool in Theory of Computation"],"prefix":"10.1145","author":[{"given":"Maria","family":"Knobelsdorf","sequence":"first","affiliation":[{"name":"Universit\u00e4t Hamburg, Hamburg, Germany"}]},{"given":"Christiane","family":"Frede","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Hamburg, Hamburg, Germany"}]},{"given":"Sebastian","family":"B\u00f6hne","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Potsdam, Potsdam, Germany"}]},{"given":"Christoph","family":"Kreitz","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Potsdam, Potsdam, Germany"}]}],"member":"320","published-online":{"date-parts":[[2017,8,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.sbspro.2010.03.399"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.005"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021871.18776.94"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207390050203360"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.79.1"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","volume-title":"Situated cognition: Social, semiotic, and psychological perspectives, Kirshner","author":"Bereiter C.","DOI":"10.4324\/9781003064121-11"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9072-3"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/979968.979970"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007996.1008002"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.3102\/0013189X018001032"},{"issue":"11","key":"e_1_3_2_1_14_1","first-page":"38","article-title":"Cognitive apprenticeship: Making thinking visible","volume":"6","author":"Collins A.","year":"1991","journal-title":"American Educator"},{"key":"e_1_3_2_1_15_1","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"R."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2361276.2361290"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2787622.2787715"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.3166\/tsi.24.1139-1160"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"V.\n      Durand-Guerrier P.\n      Boero N.\n      Douek S. S.\n      Epp and \n      D.\n      Tanguay\n  . \n  2012\n  . Examining the Role of Logic in Teaching Proof. In Proof and Proving in \n  Mathematics Education Volume \n  15\n   of \n  the series New ICMI Study Series 369--389.  V. Durand-Guerrier P. Boero N. Douek S. S. Epp and D. Tanguay. 2012. Examining the Role of Logic in Teaching Proof. In Proof and Proving in Mathematics Education Volume 15 of the series New ICMI Study Series 369--389.","DOI":"10.1007\/978-94-007-2129-6_16"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1597849.1384359"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.3166\/tsi.24.1113-1138"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207390412331271267"},{"key":"e_1_3_2_1_24_1","unstructured":"T. Hales M. Adams G. Bauer D.T. Dang J. Harrison L.T. Hoang and T. Q. Nguyen. 2015. A formal proof of the Kepler conjecture. arXiv preprint arXiv:1501.02155.  T. Hales M. Adams G. Bauer D.T. Dang J. Harrison L.T. Hoang and T. Q. Nguyen. 2015. A formal proof of the Kepler conjecture. arXiv preprint arXiv:1501.02155."},{"key":"e_1_3_2_1_25_1","volume-title":"Proceedings of the fifth Australasian conference on Computing education","volume":"20","author":"Hamilton M."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_16"},{"key":"e_1_3_2_1_27_1","volume-title":"Proceedings of the 11th annual SIGCSE conference on Innovation and technology in computer science education. ITICSE '06. ACM, 306--306","author":"Wagenknecht C."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/353485.353487"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","volume-title":"Cognition in the Wild","author":"Hutchins E.","DOI":"10.7551\/mitpress\/1881.001.0001"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2534860"},{"key":"e_1_3_2_1_31_1","unstructured":"INRIA. The Coq Webpage with a collection of teaching practices: https:\/\/coq.inria.fr\/cocorico\/CoqInTheClassroom  INRIA. The Coq Webpage with a collection of teaching practices: https:\/\/coq.inria.fr\/cocorico\/CoqInTheClassroom"},{"issue":"1","key":"e_1_3_2_1_32_1","first-page":"11","article-title":"Distributed Cognition and Educational Practice","volume":"13","author":"Karasavvidis I.","year":"2002","journal-title":"Journal of Interactive Learning Research"},{"key":"e_1_3_2_1_33_1","volume-title":"HDI","author":"Kiehn F.","year":"2017"},{"key":"e_1_3_2_1_34_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 8th International Conference on Informatics in Schools: Situation, Evolution, and Perspectives (ISSEP)","author":"Knobelsdorf M."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2960310.2960331"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2538862.2538944"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Y. Lincoln and E. Guba. 1985. Naturalistic Inquiry. Sage Publications. Newbury Park California.  Y. Lincoln and E. Guba. 1985. Naturalistic Inquiry. Sage Publications. Newbury Park California.","DOI":"10.1016\/0147-1767(85)90062-8"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"S. McKenney and C. Reeves. 2012. Conducting educational design research. New York Routledge.  S. McKenney and C. Reeves. 2012. Conducting educational design research. New York Routledge.","DOI":"10.4324\/9780203818183"},{"key":"e_1_3_2_1_39_1","article-title":"Qualitative Content Analysis. Forum","volume":"1","author":"Mayring P.","year":"2000","journal-title":"Qualitative Social Research [Online Journal]"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139567725"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","volume-title":"Knowledge in Motion","author":"Nespor J.","DOI":"10.4324\/9781315821894"},{"key":"e_1_3_2_1_42_1","volume-title":"Lecture Notes in Computer Science","volume":"2283","author":"Nipkow T."},{"key":"e_1_3_2_1_43_1","first-page":"164","article-title":"What makes big-O analysis difficult: understanding how students understand runtime analysis","volume":"29","author":"Parker M.","year":"2014","journal-title":"Journal of Computing Science in Colleges"},{"key":"e_1_3_2_1_44_1","volume-title":"Distributed cognitions: Psychological and educational considerations","author":"Pea R."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1207\/s15327809jls1303_6"},{"key":"e_1_3_2_1_46_1","unstructured":"B. Pierce etal 2017. Software Foundations. https:\/\/softwarefoundations.cis.upenn.edu\/current\/index.html  B. Pierce et al. 2017. Software Foundations. https:\/\/softwarefoundations.cis.upenn.edu\/current\/index.html"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709424.1709444"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1121341.1121459"},{"key":"e_1_3_2_1_49_1","unstructured":"S. Rychen L. H. Salganik. 2003. A holistic model of competence. In Key Competencies for a Successful Life and a Well-Functioning Society Rychen S. Salganik L. H. Ed Hogrefe & Huber Seatlle 41--62.  S. Rychen L. H. Salganik. 2003. A holistic model of competence. In Key Competencies for a Successful Life and a Well-Functioning Society Rychen S. Salganik L. H. Ed Hogrefe & Huber Seatlle 41--62."},{"key":"e_1_3_2_1_50_1","volume-title":"Proceedings of PATE'07 conference, Elsevier, 79--96","author":"Sakowicz J."},{"key":"e_1_3_2_1_51_1","volume-title":"Learning with computers","author":"S\u00e4lj\u00f6 R."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5485\/TMCS.2008.0183"},{"key":"e_1_3_2_1_53_1","unstructured":"A. H. Schoenfeld. 1994. Reflections on doing and teaching mathematics. In Mathematical thinking and problem solving Schoenfeld A. H. Ed. Routledge 53--70.  A. H. Schoenfeld. 1994. Reflections on doing and teaching mathematics. In Mathematical thinking and problem solving Schoenfeld A. H. Ed. Routledge 53--70."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1227310.1227463"},{"key":"e_1_3_2_1_55_1","volume-title":"Introduction to the Theory of Computation Cengage Learning","author":"Sipser M."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000044825.55318.95"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1080\/08993400802332332"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1080\/08993408.2013.869396"},{"key":"e_1_3_2_1_59_1","unstructured":"L. S. Vygotsky. 1978. Mind in Society: The Development of Higher Psychological Processes: Harvard University Press.  L. S. Vygotsky. 1978. Mind in Society: The Development of Higher Psychological Processes: Harvard University Press."},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015535614355"},{"key":"e_1_3_2_1_61_1","volume-title":"Voices of the Mind: Sociocultural Approach to Mediated Action","author":"Wertsch J.W."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1469-7610.1976.tb00381.x"}],"event":{"name":"ICER '17: International Computing Education Research Conference","location":"Tacoma Washington USA","acronym":"ICER '17","sponsor":["SIGCSE ACM Special Interest Group on Computer Science Education"]},"container-title":["Proceedings of the 2017 ACM Conference on International Computing Education Research"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3105726.3106184","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3105726.3106184","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:38Z","timestamp":1750217438000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3105726.3106184"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,14]]},"references-count":62,"alternative-id":["10.1145\/3105726.3106184","10.1145\/3105726"],"URL":"https:\/\/doi.org\/10.1145\/3105726.3106184","relation":{},"subject":[],"published":{"date-parts":[[2017,8,14]]},"assertion":[{"value":"2017-08-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}