{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,12,27]],"date-time":"2023-12-27T11:34:06Z","timestamp":1703676846770},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T00:00:00Z","timestamp":1181606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,8,20]]},"DOI":"10.1007\/s10817-007-9072-3","type":"journal-article","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T10:29:10Z","timestamp":1181557750000},"page":"181-218","source":"Crossref","is-referenced-by-count":18,"title":["Student Proof Exercises Using MathsTiles and Isabelle\/HOL in an Intelligent Book"],"prefix":"10.1007","volume":"39","author":[{"given":"William","family":"Billingsley","sequence":"first","affiliation":[]},{"given":"Peter","family":"Robinson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,6,12]]},"reference":[{"key":"9072_CR1","unstructured":"Abel, A., Chang, B., Pfenning, F.: Human-readable machine-verifiable proofs for teaching constructive logic. In: Egly, U., Fiedler, A., Horacek, H., and Schmitt, S. (eds.) Proceedings of the Workshop on Proof Transformations, Proof Presentations and Complexity of Proofs (PTP01) (2001)"},{"key":"9072_CR2","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1023\/B:JARS.0000021871.18776.94","volume":"32","author":"P.B. Andrews","year":"2004","unstructured":"Andrews, P.B., Brown, C.E., Pfenning, F., Bishop, M., Issar, S., Xi, H.: ETPS: a system to help students write formal proofs. J. Autom. Reason. 32, 75\u201392 (2004)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9072_CR3","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/77481.77487","volume":"33","author":"F. Arefi","year":"1990","unstructured":"Arefi, F., Hughes, C.E., Workman, D.A.: Automatically generating visual syntax-directed editors. Commun. ACM 33(3), 349\u2013360 (1990)","journal-title":"Commun. ACM"},{"key":"9072_CR4","unstructured":"Aspinall, D., L\u00fcth, C., Winterstein, D.: Parsing, editing, proving: the PGIP Display Protocol. In: International Workshop on User Interfaces for Theorem Provers 2005 (UITP\u201905) (2005)"},{"key":"9072_CR5","doi-asserted-by":"crossref","unstructured":"Baker, R.S., Corbett, A.T., Koedinger, K.R., Wagner, A.: Off-task behavior in the cognitive tutor classroom: when students \u201cgame the system.\u201d In: Dykstra-Erickson, E., Tscheligi, M. (eds.) Proceedings of ACM CHI 2004 Conference on Human Factors in Computing Systems, pp. 383\u2013390 (2004)","DOI":"10.1145\/985692.985741"},{"key":"9072_CR6","unstructured":"Ballarin, C., Klein, G.: Introduction to the Isabelle Proof Assistant. In: Second International Joint Conference on Automated Reasoning (2004). Available from http:\/\/isabelle.in.tum.de\/coursematerial\/IJCAR04\/index.html. . Accessed 24 February 2007"},{"key":"9072_CR7","volume-title":"Hyperproof","author":"J. Barwise","year":"1994","unstructured":"Barwise, J., Etchemendy, J.: Hyperproof. CSLI, Stanford, CA (1994)"},{"issue":"3","key":"9072_CR8","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1023\/B:JARS.0000044872.51237.c9","volume":"32","author":"P. Baumgartner","year":"2004","unstructured":"Baumgartner, P., Furbach, U., Gro\u00df-Hardt, M., Sinner, A.: Living book \u2013 deduction, slicing, and interaction. J. Autom. Reason. 32(3), 259\u2013286 (2004)","journal-title":"J. Autom. Reason."},{"key":"9072_CR9","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Horacek, H., Kruijff-Korbayov\u00e1, I., Pinkal, M., Siekmann, J., Wolska, M.: Natural language dialog with a tutor system for mathematical proofs. In: Lu, R., Siekmann, J., Ullrich, C. (eds.) Cognitive Systems: Joint Chinese-German Workshop, Shanghai, China, March 7\u201311, 2005, Revised Selected Papers, pp. 1\u201314 (2007)","DOI":"10.1007\/978-3-540-70934-3_1"},{"key":"9072_CR10","unstructured":"Benzm\u00fcller, C., Horacek, H., Lesourd, H., Kruijff-Korbayova, I., Schiller, M., Wolska, M.: A corpus of tutorial dialogs on theorem proving; the influence of the presentation of the study-material. In: Proceedings of International Conference on Language Resources and Evaluation (LREC 2006). Genova, Italy (2006)"},{"key":"9072_CR11","unstructured":"Billingsley, W., Billingsley, J.: The animation of simulations and tutorial clients for online teaching. In: Proceedings of the 15th Annual Conference for the Australasian Association for Engineering Education and the 10th Australasian Women in Engineering Forum, pp. 532\u2013540. Toowoomba, Australia(2004)"},{"key":"9072_CR12","unstructured":"Billingsley, W., Robinson, P., Ashdown, M., Hanson, C.: Intelligent tutoring and supervised problem solving in the browser. In: Proceedings of the IADIS International Conference WWW\/Internet 2004, pp. 806\u2013811. Madrid, Spain (2004)"},{"key":"9072_CR13","doi-asserted-by":"crossref","unstructured":"Blackwell, A., Green, T.: Notational systems - the cognitive dimensions of notations framework. In: Carroll, J.M. (ed.) HCI Models, Theories and Frameworks, pp. 103\u2013133. Amsterdam (2003)","DOI":"10.1016\/B978-155860808-5\/50005-8"},{"key":"9072_CR14","unstructured":"Blackwell, A., Green, T.: A cognitive dimensions questionnaire. (2007) Available online from http:\/\/www.cl.cam.ac.uk\/~afb21\/CognitiveDimensions\/CDquestionnaire.pdf. . Accessed 25 February 2007"},{"key":"9072_CR15","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1016\/S0020-7373(75)80026-5","volume":"7","author":"J.S. Brown","year":"1975","unstructured":"Brown, J.S., Burton, R.R., Bell, A.G.: SOPHIE: a step towards a reactive learning environment. Int. J. Man-Machine Stud. 7, 675\u2013696 (1975)","journal-title":"Int. J. Man-Machine Stud."},{"key":"9072_CR16","unstructured":"Clark, J. (ed.).: XSL Transformations (XSLT) Version 1.0. World Wide Web Consortium (1999). Accessed 13 August 2006 from http:\/\/www.w3.org\/TR\/1999\/REC-xslt-19991116"},{"key":"9072_CR17","unstructured":"Clark, J., DeRose, S. (eds.).: XML Path Language (XPath) Version 1.0. World Wide Web Consortium (1999). Accessed 30 January 2005 from http:\/\/www.w3.org\/TR\/1999\/REC-xpath-19991116"},{"issue":"4","key":"9072_CR18","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1023\/A:1021258506583","volume":"12","author":"C. Conati","year":"2002","unstructured":"Conati, C., Gertner, A.S., VanLehn, K.: Using Bayesian networks to manage uncertainty in student modeling. User Model. User-Adapted Interact. 12(4), 371\u2013417 (2002)","journal-title":"User Model. User-Adapted Interact."},{"key":"9072_CR19","doi-asserted-by":"crossref","unstructured":"Craig, S.D., Hu, X., Gholson, B., Marks, W., Graesser, A.C., Group, T.T.R.: AutoTutor: a human tutoring simulation with an animated pedagogical interface. In: Hamberger, P. (ed.) Proceedings of the International Society for Optical Engineering: Integrated Command Environments (2000)","DOI":"10.1117\/12.407538"},{"key":"9072_CR20","doi-asserted-by":"crossref","unstructured":"Ehrensburger, J., Zinn, C.: DiaLog: a system for dialogue logic. In: Conference on Automated Deduction, pp. 446\u2013460, (1997)","DOI":"10.1007\/3-540-63104-6_44"},{"key":"9072_CR21","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1006\/jvlc.1996.0009","volume":"7","author":"T.R.G. Green","year":"1996","unstructured":"Green, T.R.G., Petre, M.: Usability analysis of visual programming environments. J. Vis. Lang. Comput. 7, 131\u2013174 (1996)","journal-title":"J. Vis. Lang. Comput."},{"key":"9072_CR22","doi-asserted-by":"crossref","unstructured":"Hansen, W.J.: Creation of hierarchic text with a computer display. Technical report, Argonne National Laboratories (1971)","DOI":"10.2172\/4721186"},{"key":"9072_CR23","unstructured":"Kelleher, C., Cosgrove, D., Culyba, D., Forlines, C., Pratt, J., Pausch, R.: Alice2: programming without syntax errors. In: User Interface Software and Technology. Paris (2002)"},{"key":"9072_CR24","doi-asserted-by":"crossref","unstructured":"Khwaja, A.A., Urban, J.E.: Syntax-directed editing environments: issues and features. In: SAC \u201993: Proceedings of the 1993 ACM\/SIGAPP symposium on Applied computing, pp. 230\u2013237. New York, NY, USA (1993)","DOI":"10.1145\/162754.162882"},{"key":"9072_CR25","doi-asserted-by":"crossref","unstructured":"Ko, A.J., Aung, H., Myers, B.A.: Eliciting design requirements for maintenance-oriented IDEs: A detailed study of corrective and perfective maintenance tasks. In: International Conference on Software Engineering (2005)","DOI":"10.1145\/1062455.1062492"},{"key":"9072_CR26","doi-asserted-by":"crossref","unstructured":"Kohlhase, M.: OMDoc: towards an Internet standard for the administration, distribution and teaching of mathematical knowledge. In: AISC 2000 Artificial Intelligence and Symbolic Computation Theory. pp. 32\u201352 (2000)","DOI":"10.1007\/3-540-44990-6_3"},{"issue":"7","key":"9072_CR27","doi-asserted-by":"crossref","first-page":"600","DOI":"10.1080\/00029890.1995.12004627","volume":"102","author":"L. Lamport","year":"1995","unstructured":"Lamport, L.: How to write a proof. Amer. Math. Monthly 102(7), 600\u2013608 (1995)","journal-title":"Amer. Math. Monthly"},{"key":"9072_CR28","unstructured":"Lesa, L., Yacef, K.: An intelligent teaching system for logic. In: Intelligent Tutoring Systems : 6th International Conference, ITS 2002, Biarritz, France and San Sebastian, Spain, June 2\u20137, (2002)"},{"key":"9072_CR29","doi-asserted-by":"crossref","unstructured":"Lukins, S., Levicki, A., Burg, J.: A tutorial program for propositional logic with human\/computer interactive learning. In: Proceedings of the 33rd SIGCSE Technical Symposium on Computer Science Education, pp. 381\u2013385, (2002)","DOI":"10.1145\/563340.563490"},{"issue":"4","key":"9072_CR30","first-page":"385","volume":"12","author":"E. Melis","year":"2001","unstructured":"Melis, E., Andr\u00e8s, E., B\u00fcdenbender, J., Frischauf, A., Goguadze, G., Libbrecht, P., Pollet, M., Ullrich, C.: Activemath: a generic and adaptive web-based learning environment. Int. J. Artif. Intell. Educ 12(4), 385\u2013407 (2001)","journal-title":"Int. J. Artif. Intell. Educ"},{"issue":"2","key":"9072_CR31","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1080\/1049482940040202","volume":"4","author":"P. Miller","year":"1994","unstructured":"Miller, P., Pane, J., Meter, G., Vorthmann, S.: Evolution of novice programming environments: the structure editors of Carnegie Mellon University. Interact. Learn. Environ. 4(2), 140\u2013158 (1994)","journal-title":"Interact. Learn. Environ."},{"key":"9072_CR32","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Structured proofs in Isar\/HOL. In: Geuvers, H., Wiedijk, F. (eds.) Types for Proofs and Programs (TYPES 2002), pp. 259\u2013278, (2003). Also available online from http:\/\/www4.informatik.tu-muenchen.de\/~nipkow\/pubs\/types02.pdf accessed 10 June 2005","DOI":"10.1007\/3-540-39185-1_15"},{"key":"9072_CR33","unstructured":"Nipkow, T.: A compact introduction to Isabelle\/HOL. (2006). Available from http:\/\/isabelle.in.tum.de\/coursematerial\/Shanghai06\/index.html. . Accessed 24 February 2007"},{"key":"9072_CR34","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Berlin Heidelberg New York (2002)"},{"key":"9072_CR35","doi-asserted-by":"crossref","unstructured":"Rehman, K., Billingsley, W., Robinson, P.: Writing questions for an Intelligent Book using external AI. In: Proceedings of the Sixth International Conference on Advanced Learning Technologies (ICALT2006), pp. 1089\u20131091, (2006)","DOI":"10.1109\/ICALT.2006.1652638"},{"issue":"2","key":"9072_CR36","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1080\/1049482940040203","volume":"4","author":"R. Scheines","year":"1994","unstructured":"Scheines, R., Sieg, W.: Computer environments for proof construction. Interact. Learn. Environ. 4(2), 159\u2013169 (1994)","journal-title":"Interact. Learn. Environ."},{"key":"9072_CR37","unstructured":"Slind, K., Barrus, S., Choe, S., Condrat, C., Duan, J., Gopalakrishnan, S., Knoll, A., Kuwahara, H., Li, G., Little, S., Liu, L., Moore, S., Palmer, R., Tuttle, C., Walton, S., Yang, Y., Zhang, J.: Teaching a HOL course: Experience report. In: Hurd, J., Smith, E., Darbari, A. (eds.) Theorem Proving in Higher Order Logics: Emerging Trends Proceedings, pp. 170\u2013179, (2005)"},{"key":"9072_CR38","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1023\/B:JARS.0000044825.55318.95","volume":"32","author":"R. Sommer","year":"2004","unstructured":"Sommer, R., Nuckols, G.: A proof environment for teaching aathematics. J. Autom. Reason. 32, 227\u2013258 (2004)","journal-title":"J. Autom. Reason."},{"key":"9072_CR39","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0004-3702(77)90029-7","volume":"9","author":"R. Stallman","year":"1977","unstructured":"Stallman, R., Sussman, G.J.: Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artif. Intell. 9, 135\u2013196 (1977)","journal-title":"Artif. Intell."},{"issue":"9","key":"9072_CR40","doi-asserted-by":"crossref","first-page":"563","DOI":"10.1145\/358746.358755","volume":"24","author":"T. Teitelbaum","year":"1981","unstructured":"Teitelbaum, T., Reps, T.: The Cornell Program Synthesizer: a syntax-directed programming environment. Commun. ACM 24(9), 563\u2013573 (1981)","journal-title":"Commun. ACM"},{"key":"9072_CR41","doi-asserted-by":"crossref","unstructured":"Van Der\u00a0Hoeven, J.: GNU TeXmacs: a free, structured, wysiwyg and technical text editor. Le document au XXI-i\u00e8me si\u00e8cle 39\u201340, 39\u201350 (2001)","DOI":"10.5802\/cg.292"},{"key":"9072_CR42","unstructured":"Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs\u201999 (1999). Also available online from http:\/\/www4.in.tum.de\/~wenzelm\/papers\/Isar-TPHOLs99.pdf accessed 10 June 2005"},{"key":"9072_CR43","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: The Isabelle\/Isar Reference Manual. TU M\u00fcnchen (2005)","DOI":"10.1007\/11542384_8"},{"key":"9072_CR44","volume-title":"Types for Proofs and Programs, LNCS, vol. 3085\/2004","author":"F. Wiedijk","year":"2004","unstructured":"Wiedijk, F.: Formal proof sketches. In: Types for Proofs and Programs, LNCS, vol. 3085\/2004. Springer, Berlin Heidelberg New York (2004)"},{"key":"9072_CR45","unstructured":"Winer, D.: XML-RPC Specification. UserLand Software. (1999) Accessed 30 January 2005 from http:\/\/www.xmlrpc.com\/spec"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9072-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-007-9072-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9072-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:47Z","timestamp":1559265707000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-007-9072-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6,12]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2007,8,20]]}},"alternative-id":["9072"],"URL":"https:\/\/doi.org\/10.1007\/s10817-007-9072-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,6,12]]}}}