Student proof exercises using MathsTiles and Isabelle/HOL in an intelligent book. (English) Zbl 1129.68499

Summary: The Intelligent Book project aims to improve online education by designing materials that can model the subject matter they teach, in the manner of a reactive learning environment. In this paper, we investigate using an automated proof assistant, particularly Isabelle/HOL, as the model supporting first year undergraduate exercises in which students write proofs in number theory. Automated proof assistants are generally considered to be difficult for novices to learn. We examine whether, by providing a very specialized interface, it is possible to build something that is usable enough to be of educational value. To ensure students cannot “game the system” the exercise avoids tactic-choosing interaction styles but asks the student to write out the proof. Proofs are written using MathsTiles: composable tiles that resemble written mathematics. Unlike traditional syntax-directed editors, MathsTiles allows students to keep many answer fragments on the canvas at the same time and does not constrain the order in which an answer is written. Also, the tile syntax does not need to match the underlying Isar syntax exactly, and different tiles can be used for different questions. The exercises take place within the context of an Intelligent Book. We performed a user study and qualitative analysis of the system. Some users were able to complete proofs with much less training than is usual for the automated proof assistant itself, but there remain significant usability issues to overcome.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI Link


[1] 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)
[2] 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–92 (2004) · Zbl 02081545
[3] Arefi, F., Hughes, C.E., Workman, D.A.: Automatically generating visual syntax-directed editors. Commun. ACM 33(3), 349–360 (1990)
[4] Aspinall, D., Lüth, C., Winterstein, D.: Parsing, editing, proving: the PGIP Display Protocol. In: International Workshop on User Interfaces for Theorem Provers 2005 (UITP’05) (2005)
[5] Baker, R.S., Corbett, A.T., Koedinger, K.R., Wagner, A.: Off-task behavior in the cognitive tutor classroom: when students ”game the system.” In: Dykstra-Erickson, E., Tscheligi, M. (eds.) Proceedings of ACM CHI 2004 Conference on Human Factors in Computing Systems, pp. 383–390 (2004)
[6] 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
[7] Barwise, J., Etchemendy, J.: Hyperproof. CSLI, Stanford, CA (1994)
[8] Baumgartner, P., Furbach, U., Groß-Hardt, M., Sinner, A.: Living book – deduction, slicing, and interaction. J. Autom. Reason. 32(3), 259–286 (2004) · Zbl 02129477
[9] Benzmüller, C., Horacek, H., Kruijff-Korbayová, 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–11, 2005, Revised Selected Papers, pp. 1–14 (2007)
[10] Benzmüller, 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)
[11] 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–540. Toowoomba, Australia(2004)
[12] 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–811. Madrid, Spain (2004)
[13] Blackwell, A., Green, T.: Notational systems - the cognitive dimensions of notations framework. In: Carroll, J.M. (ed.) HCI Models, Theories and Frameworks, pp. 103–133. Amsterdam (2003)
[14] Blackwell, A., Green, T.: A cognitive dimensions questionnaire. (2007) Available online from http://www.cl.cam.ac.uk/\(\sim\)afb21/CognitiveDimensions/CDquestionnaire.pdf. . Accessed 25 February 2007
[15] Brown, J.S., Burton, R.R., Bell, A.G.: SOPHIE: a step towards a reactive learning environment. Int. J. Man-Machine Stud. 7, 675–696 (1975) · Zbl 0306.68060
[16] 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
[17] 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
[18] Conati, C., Gertner, A.S., VanLehn, K.: Using Bayesian networks to manage uncertainty in student modeling. User Model. User-Adapted Interact. 12(4), 371–417 (2002) · Zbl 1030.68630
[19] 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)
[20] Ehrensburger, J., Zinn, C.: DiaLog: a system for dialogue logic. In: Conference on Automated Deduction, pp. 446–460, (1997)
[21] Green, T.R.G., Petre, M.: Usability analysis of visual programming environments. J. Vis. Lang. Comput. 7, 131–174 (1996)
[22] Hansen, W.J.: Creation of hierarchic text with a computer display. Technical report, Argonne National Laboratories (1971)
[23] 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)
[24] Khwaja, A.A., Urban, J.E.: Syntax-directed editing environments: issues and features. In: SAC ’93: Proceedings of the 1993 ACM/SIGAPP symposium on Applied computing, pp. 230–237. New York, NY, USA (1993)
[25] 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)
[26] 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–52 (2000) · Zbl 1042.00511
[27] Lamport, L.: How to write a proof. Amer. Math. Monthly 102(7), 600–608 (1995) · Zbl 0877.00005
[28] 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–7, (2002) · Zbl 1045.68791
[29] 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–385, (2002)
[30] Melis, E., Andrès, E., Büdenbender, 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–407 (2001)
[31] 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–158 (1994) · Zbl 02314695
[32] Nipkow, T.: Structured proofs in Isar/HOL. In: Geuvers, H., Wiedijk, F. (eds.) Types for Proofs and Programs (TYPES 2002), pp. 259–278, (2003). Also available online from http://www4.informatik.tu-muenchen.de/\(\sim\)nipkow/pubs/types02.pdf accessed 10 June 2005
[33] Nipkow, T.: A compact introduction to Isabelle/HOL. (2006). Available from http://isabelle.in.tum.de/coursematerial/Shanghai06/index.html. . Accessed 24 February 2007
[34] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Berlin Heidelberg New York (2002) · Zbl 0994.68131
[35] 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–1091, (2006)
[36] Scheines, R., Sieg, W.: Computer environments for proof construction. Interact. Learn. Environ. 4(2), 159–169 (1994) · Zbl 02314696
[37] 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–179, (2005)
[38] Sommer, R., Nuckols, G.: A proof environment for teaching aathematics. J. Autom. Reason. 32, 227–258 (2004) · Zbl 02129476
[39] Stallman, R., Sussman, G.J.: Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artif. Intell. 9, 135–196 (1977) · Zbl 0372.94024
[40] Teitelbaum, T., Reps, T.: The Cornell Program Synthesizer: a syntax-directed programming environment. Commun. ACM 24(9), 563–573 (1981)
[41] Van Der Hoeven, J.: GNU TeXmacs: a free, structured, wysiwyg and technical text editor. Le document au XXI-ième siècle 39–40, 39–50 (2001)
[42] Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99 (1999). Also available online from http://www4.in.tum.de/\(\sim\)wenzelm/papers/Isar-TPHOLs99.pdf accessed 10 June 2005
[43] Wenzel, M.: The Isabelle/Isar Reference Manual. TU München (2005)
[44] Wiedijk, F.: Formal proof sketches. In: Types for Proofs and Programs, LNCS, vol. 3085/2004. Springer, Berlin Heidelberg New York (2004) · Zbl 1100.68620
[45] Winer, D.: XML-RPC Specification. UserLand Software. (1999) Accessed 30 January 2005 from http://www.xmlrpc.com/spec
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.