{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:56:10Z","timestamp":1725936970688},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319737201"},{"type":"electronic","value":"9783319737218"}],"license":[{"start":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T00:00:00Z","timestamp":1514505600000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-73721-8_7","type":"book-chapter","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T04:13:05Z","timestamp":1514434385000},"page":"138-160","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Framework for Computer-Aided Design of Educational Domain Models"],"prefix":"10.1007","author":[{"given":"Eric","family":"Butler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zoran","family":"Popovi\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,29]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Andersen, E., Gulwani, S., Popovi\u0107, Z.: A trace-based framework for analyzing and synthesizing educational progressions. In: CHI (2013)","DOI":"10.1145\/2470654.2470764"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"O\u2019Rourke, E., Andersen, E., Gulwani, S., Popovi\u0107, Z.: A framework for automatically generating interactive instructional scaffolding. In: Proceedings of the 33rd Annual ACM Conference on Human Factors in Computing Systems, CHI 2015, pp. 1545\u20131554. ACM, New York (2015)","DOI":"10.1145\/2702123.2702580"},{"issue":"2","key":"7_CR3","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1207\/s15327809jls0402_2","volume":"4","author":"JR Anderson","year":"1995","unstructured":"Anderson, J.R., Corbett, A.T., Koedinger, K.R., Pelletier, R.: Cognitive tutors: Lessons learned. The Journal of the Learning Sciences 4(2), 167\u2013207 (1995)","journal-title":"The Journal of the Learning Sciences"},{"key":"7_CR4","unstructured":"VanLehn, K.: Mind bugs: The origins of procedural misconceptions. MIT press (1990)"},{"key":"7_CR5","unstructured":"Murray, T.: Authoring intelligent tutoring systems: An analysis of the state of the art. International Journal of Artificial Intelligence in Education 10 (1999)"},{"issue":"2","key":"7_CR6","first-page":"8:1","volume":"22","author":"YE Liu","year":"2015","unstructured":"Liu, Y.E., Ballweber, C., O\u2019rourke, E., Butler, E., Thummaphan, P., Popovi\u0107, Z.: Large-scale educational campaigns. ACM Trans. Comput.-Hum. Interact. 22(2), 8:1\u20138:24 (2015)","journal-title":"ACM Trans. Comput.-Hum. Interact."},{"issue":"1","key":"7_CR7","first-page":"32","volume":"39","author":"J Demski","year":"2012","unstructured":"Demski, J.: This time it\u2019s personal: True student-centered learning has a lot of support from education leaders, but it can\u2019t really happen without all the right technology infrastructure to drive it. and the technology just may be ready to deliver on its promise. THE Journal (Technological Horizons In Education) 39(1), 32 (2012)","journal-title":"THE Journal (Technological Horizons In Education)"},{"key":"7_CR8","unstructured":"Redding, S.: Getting personal: the promise of personalized learning. In: Handbook on Innovations in Learning, pp. 113\u2013130 (2013)"},{"key":"7_CR9","unstructured":"Charles, R.I., Hall, B., Kennedy, D., Bellman, A.E., Bragg, S.C., Handlin, W.G., Murphy, S.J., Wiggins, G.: Algebra 1: Common Core. Pearson Education, Inc. (2012)"},{"issue":"2","key":"7_CR10","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1207\/s15516709cog1202_4","volume":"12","author":"J Sweller","year":"1988","unstructured":"Sweller, J.: Cognitive load during problem solving: Effects on learning. Cognitive Science 12(2), 257\u2013285 (1988)","journal-title":"Cognitive Science"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: Proceedings of the 12th Inter. Conf. on Architectural Support for Programming Languages and Operating Systems. ACM (2006)","DOI":"10.1145\/1168857.1168907"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Torlak, E., Bodik, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (2014)","DOI":"10.1145\/2666356.2594340"},{"key":"7_CR13","unstructured":"Alur, R., Bod\u00edk, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, pp. 1\u201325 (2015)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Handbook of Theoretical Computer Science, vol. b, pp. 243\u2013320. MIT Press, Cambridge (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-319-39583-8_36","volume-title":"Intelligent Tutoring Systems","author":"E Butler","year":"2016","unstructured":"Butler, E., Torlak, E., Popovi\u0107, Z.: A framework for parameterized design of rule systems applied to algebra. In: Micarelli, A., Stamper, J., Panourgia, K. (eds.) ITS 2016. LNCS, vol. 9684, pp. 320\u2013326. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-39583-8_36"},{"key":"7_CR16","volume-title":"The Calculus of Computation: Decision Procedures with Applications to Verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag, New York Inc (2007)"},{"key":"7_CR17","unstructured":"Butler, E., Torlak, E., Popovic, Z.: Synthesizing optimal domain models for educational applications. Technical Report UW-CSE-17-10-02, University of Washington (2017). https:\/\/www.cs.washington.edu\/tr\/2017\/10\/UW-CSE-17-10-02.pdf"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"7_CR19","unstructured":"Butler, E., Torlak, E., Popovic, Z.: Rulesy source code and data. https:\/\/github.com\/edbutler\/nonograms-rule-synthesis"},{"key":"7_CR20","first-page":"805","volume":"2","author":"G Harel","year":"2007","unstructured":"Harel, G., Sowder, L.: Toward comprehensive perspectives on the learning and teaching of proof. Second Handbook of Research on Mathematics Teaching and Learning 2, 805\u2013842 (2007)","journal-title":"Second Handbook of Research on Mathematics Teaching and Learning"},{"issue":"2","key":"7_CR21","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/j.cogsys.2006.07.004","volume":"10","author":"P Langley","year":"2009","unstructured":"Langley, P., Laird, J.E., Rogers, S.: Cognitive architectures: Research issues and challenges. Cognitive Systems Research 10(2), 141\u2013160 (2009)","journal-title":"Cognitive Systems Research"},{"issue":"1","key":"7_CR22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(87)90050-6","volume":"33","author":"JE Laird","year":"1987","unstructured":"Laird, J.E., Newell, A., Rosenbloom, P.S.: Soar: An architecture for general intelligence. Artificial Intelligence 33(1), 1\u201364 (1987)","journal-title":"Artificial Intelligence"},{"key":"7_CR23","unstructured":"Anderson, J.R., Lebiere, C.: The atomic components of thought (1998)"},{"issue":"1","key":"7_CR24","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0004-3702(85)90012-8","volume":"26","author":"RE Korf","year":"1985","unstructured":"Korf, R.E.: Macro-operators: A weak method for learning. Artificial Intelligence 26(1), 35\u201377 (1985)","journal-title":"Artificial Intelligence"},{"issue":"3","key":"7_CR25","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1609\/aimag.v34i3.2484","volume":"34","author":"KR Koedinger","year":"2013","unstructured":"Koedinger, K.R., Brunskill, E., Baker, R.S., McLaughlin, E.A., Stamper, J.: New potentials for data-driven intelligent tutoring system development and optimization. AI Magazine 34(3), 27\u201341 (2013)","journal-title":"AI Magazine"},{"key":"7_CR26","unstructured":"Matsuda, N., Cohen, W.W., Koedinger, K.R.: Applying programming by demonstration in an intelligent authoring tool for cognitive tutors. In: Aaai Workshop on Human Comprehensible Machine Learning (technical report ws-05-04), pp. 1\u20138 (2005)"},{"key":"7_CR27","unstructured":"Li, N., Cohen, W., Koedinger, K.R., Matsuda, N.: A machine learning approach for automatic student model discovery. In: Educational Data Mining 2011 (2010)"},{"key":"7_CR28","unstructured":"Li, N., Schreiber, A.J., Cohen, W., Koedinger, K.: Efficient complex skill acquisition through representation learning. Advances in Cognitive Systems 2 (2012)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/978-3-540-30139-4_51","volume-title":"Intelligent Tutoring Systems","author":"MP Jarvis","year":"2004","unstructured":"Jarvis, M.P., Nuzzo-Jones, G., Heffernan, N.T.: Applying machine learning techniques to rule generation in intelligent tutoring systems. In: Lester, J.C., Vicari, R.M., Paragua\u00e7u, F. (eds.) ITS 2004. LNCS, vol. 3220, pp. 541\u2013553. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30139-4_51"},{"issue":"3","key":"7_CR30","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/j.cogsys.2010.12.002","volume":"12","author":"U Schmid","year":"2011","unstructured":"Schmid, U., Kitzelmann, E.: Inductive rule learning on the knowledge level. Cognitive Systems Research 12(3), 237\u2013248 (2011)","journal-title":"Cognitive Systems Research"},{"issue":"8","key":"7_CR31","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1145\/2634273","volume":"57","author":"S Gulwani","year":"2014","unstructured":"Gulwani, S.: Example-based learning in computer-aided stem education. Communications of the ACM 57(8), 70\u201380 (2014)","journal-title":"Communications of the ACM"},{"key":"7_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-319-07221-0_38","volume-title":"Intelligent Tutoring Systems","author":"T Lazar","year":"2014","unstructured":"Lazar, T., Bratko, I.: Data-driven program synthesis for hint generation in programming tutors. In: Trausan-Matu, S., Boyer, K.E., Crosby, M., Panourgia, K. (eds.) ITS 2014. LNCS, vol. 8474, pp. 306\u2013311. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07221-0_38"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (2013)","DOI":"10.1145\/2491956.2462195"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Tillmann, N., de Halleux, J., Xie, T., Bishop, J.: Constructing coding duels in Pex4Fun and Code Hunt. In: ISSTA, pp. 445\u2013448. ACM (2014)","DOI":"10.1145\/2610384.2628054"},{"key":"7_CR35","unstructured":"Lee, C.: DeduceIt: a tool for representing and evaluating student derivations. Stanford Digital Repository (2012). http:\/\/purl.stanford.edu\/bg823wn2892"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Polozov, O., Gulwani, S.: Flashmeta: a framework for inductive program synthesis. In: Proceedings of the 2015 ACM SIGPLAN Inter. Conf. on Object-Oriented Programming, Systems, Languages, and Applications, pp. 107\u2013126. ACM (2015)","DOI":"10.1145\/2814270.2814310"},{"key":"7_CR37","unstructured":"Liang, P., Jordan, M.I., Klein, D.: Learning programs: a hierarchical bayesian approach. In: Proceedings of the 27th International Conference on Machine Learning (ICML 2010), pp. 639\u2013646 (2010)"},{"key":"7_CR38","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. Citeseer (1989)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 151\u2013157. ACM (1978)","DOI":"10.1145\/512760.512776"},{"issue":"1","key":"7_CR40","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1145\/1707801.1706325","volume":"45","author":"P Suter","year":"2010","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. ACM Sigplan Notices 45(1), 199\u2013210 (2010)","journal-title":"ACM Sigplan Notices"},{"issue":"8","key":"7_CR41","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/j.entcs.2006.11.037","volume":"174","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of recursive data types. Electronic Notes in Theoretical Computer Science 174(8), 23\u201337 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73721-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T16:01:05Z","timestamp":1570550465000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73721-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,29]]},"ISBN":["9783319737201","9783319737218"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73721-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017,12,29]]}}}