References

  1. Andreas Abel, Bor-Yuh Evan Chang & Frank Pfenning (2001): Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic. In: Uwe Egly, A. Fiedler, Helmut Horacek & Stephan Schmitt: Proceedings of the Workshop on Proof Transformations, Proof Presentations and Complexity of Proofs (PTP'01). Universitá degli studi di Siena.
  2. Vincent Aleven & Kenneth Koedinger (2000): Limitations of Student Control: Do Students Know when They Need Help?. In: Gilles Gauthier, Claude Frasson & Kurt VanLehn: Intelligent Tutoring Systems, Lecture Notes in Computer Science 1839. Springer Berlin / Heidelberg, pp. 292–303. Available at http://dx.doi.org/10.1007/3-540-45108-0_33.
  3. John Robert Anderson (1993): Rules of the mind. Lawrence Erlbaum Associates, Hillsdale, NJ.
  4. Peter B. Andrews (1980): Transforming matings into natural deduction proofs. In: Proceedings of the 5th Conference on Automated Deduction (CADE), LNCS 87. Springer, pp. 375–393. Available at http://dx.doi.org/10.1007/3-540-10009-1_22.
  5. Kevin D. Ashley, Ravi Desai & John M. Levine (2002): Teaching Case-Based Argumentation Concepts using Dialectic Arguments vs. Didactic Explanations. In: In Proceedings of the Intelligent Tutoring Systems Conference. Springer, pp. 585–595. Available at http://dx.doi.org/10.1007/3-540-47987-2_60.
  6. David Aspinall, Ewen Denney & Christoph Lüth (2010): Tactics for Hierarchical Proofs. Journal Mathematics in Computer Science 3, pp. 309–330. Available at http://dx.doi.org/10.1007/s11786-010-0025-6.
  7. Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier & Claus-Peter Wirth (2006): A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity. In: Kohlhase, pp. 126–142. Available at http://dx.doi.org/10.1007/11618027_9.
  8. Serge Autexier & Dominik Dietrich (2010): A Tactic Language for Declarative Proofs. In: Matt Kaufmann & Lawrence C. Paulson: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, Lecture Notes in Computer Science 6172. Springer, pp. 99–114. Available at http://dx.doi.org/10.1007/978-3-642-14052-5_9.
  9. Serge Autexier & Armin Fiedler (2006): Textbook Proofs Meet Formal Logic - The Problem of Underspecification and Granularity. In: Kohlhase, pp. 96–110. Available at http://dx.doi.org/10.1007/11618027_7.
  10. Ralph-Johan Back (2010): Structured derivations: a unified proof style for teaching mathematics. Formal Asp. Comput. 22(5), pp. 629–661. Available at http://dx.doi.org/10.1007/s00165-009-0136-5.
  11. Ralph-Johan Back, Jim Grundy & Joakim von Wright (1997): Structured Calculational Proof. Formal Asp. Comput. 9(5-6), pp. 469–483. Available at http://dx.doi.org/10.1007/BF01211456.
  12. Tiffany Barnes & John C. Stamper (2008): Toward Automatic Hint Generation for Logic Proof Tutoring Using Historical Student Data. In: Beverly Park Woolf, Esma A\"ımeur, Roger Nkambou & Susanne P. Lajoie: Intelligent Tutoring Systems, 9th International Conference, ITS 2008, Montreal, Canada, June 23-27, 2008, Proceedings, Lecture Notes in Computer Science 5091. Springer, pp. 373–382. Available at http://dx.doi.org/10.1007/978-3-540-69132-7_41.
  13. Tiffany Barnes & John C. Stamper (2010): Automatic Hint Generation for Logic Proof Tutoring Using Historical Data. Educational Technology & Society 13(1), pp. 3–12.
  14. Michael Beeson (1992): Mathpert: Computer Support for Learning Algebra, Trig, and Calculus.. In: Andrei Voronkov: LPAR, Lecture Notes in Computer Science 624. Springer, pp. 454–456. Available at http://dx.doi.org/10.1007/BFb0013085.
  15. Christoph Benzmüller, Dominik Dietrich, Marvin Schiller & Serge Autexier (2007): Deep Inference for Automated Proof Tutoring. In: Joachim Hertzberg, Michael Beetz & Roman Englert: KI 2007: Advances in Artificial Intelligence. 30th Annual German Conference on AI, LNAI 4667. Springer, pp. 435–439. Available at http://dx.doi.org/10.1007/978-3-540-74565-5_34.
  16. Christoph Benzmüller, Helmut Horacek, Henri Lesourd, Ivana Kruijff-Korbayová, Marvin Schiller & Magdalena Wolska (2006): 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). ELDA, Genova, Italy.
  17. Christoph Benzmüller, Helmut Horacek, Henri Lesourd, Ivana Kruijff-Korbayová, Marvin Schiller & Magdalena Wolska (2006): DiaWOz-II - A tool for wizard-of-oz experiments in mathematics. In: Christian Freksa, Michael Kohlhase & Kerstin Schill: KI 2006: Advances in Artificial Intelligence. 29th Annual German Conference on AI, LNAI 4314. Springer. Available at http://dx.doi.org/10.1007/978-3-540-69912-5_13.
  18. Yves Bertot, Gilles Dowek, André Hirschowitz, C. Paulin & Laurent Théry (1999): Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings. Lecture Notes in Computer Science 1690. Springer. Available at http://dx.doi.org/10.1007/3-540-48256-3.
  19. William Billingsley & Peter Robinson (2007): Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book. J. Autom. Reasoning 39(2), pp. 181–218. Available at http://dx.doi.org/10.1007/s10817-007-9072-3.
  20. John Seely Brown & Kurt VanLehn (1980): Repair theory: A generative theory of bugs in procedural skills. In: Cognitive Science 4, pp. 379–426. Available at http://dx.doi.org/10.1207/s15516709cog0404_3.
  21. Stefano A. Cerri, Guy Gouardères & Fábio Paraguaçu (2002): Intelligent Tutoring Systems, 6th International Conference, ITS 2002, Biarritz, France and San Sebastian, Spain, June 2-7, 2002, Proceedings. Lecture Notes in Computer Science 2363. Springer. Available at http://dx.doi.org/10.1007/3-540-47987-2.
  22. Lassaad Cheikhrouhou & Volker Sorge (2000): PDS – A Three-Dimensional Data Structure for Proof Plans. In: Proceedings of the International Conference on Artificial and Computational Intelligence For Decision, Control and Automation In Engineering and Industrial Applications (ACIDCA) 2000.
  23. Michelene T. H. Chi, Nicholas De Leeuw, Mei hung Chiu & Christian Lavancher (1994): Eliciting self-explanations improves understanding. Cognitive Science 18, pp. 439–477. Available at http://dx.doi.org/10.1207/s15516709cog1803_3.
  24. Koen Claessen & Niklas Sörensson (2003): New Techniques that Improve MACE-style Finite Model Finding. In: Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications.
  25. Albert Corbett (2001): Cognitive Computer Tutors: Solving the Two-Sigma Problem. In: Mathias Bauer, Piotr Gmytrasiewicz & Julita Vassileva: User Modeling 2001, Lecture Notes in Computer Science 2109. Springer Berlin / Heidelberg, pp. 137–147. Available at http://dx.doi.org/10.1007/3-540-44566-8_14.
  26. Pierre Corbineau (2007): A Declarative Language for the Coq Proof Assistant. In: Marino Miculan, Ivan Scagnetto & Furio Honsell: Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers, Lecture Notes in Computer Science 4941. Springer, pp. 69–84. Available at http://dx.doi.org/10.1007/978-3-540-68103-8_5.
  27. Ewen Denney, John Power & Konstantinos Tourlas (2006): Hiproofs: A Hierarchical Notion of Proof Tree. In: Proc. of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), Birmingham, UK, May 18-21, 2005, ENTCS 155. Elsevier, pp. 341–359. Available at http://dx.doi.org/10.1016/j.entcs.2005.11.063.
  28. Louise A. Dennis, Mateja Jamnik & Martin Pollet (2006): On the Comparison of Proof Planning Systems: lambdaCLAM, OMEGA and IsaPlanner. Electr. Notes Theor. Comput. Sci. 151(1), pp. 93–110. Available at http://dx.doi.org/10.1016/j.entcs.2005.11.025.
  29. Dominik Dietrich (2010): Assertion Level Proof Planning with Compiled Strategies. Saarland University.
  30. Dominik Dietrich & Mark Buckley (2008): Verification of Human-level Proof Steps in Mathematics Education. Teaching Mathematics and Computer Science 6(2), pp. 345–362.
  31. Dominik Dietrich & Ewaryst Schulz (2009): Integrating Structured Queries into a Tactic Language. JAL - Special issue on Programming Languages and Mechanized Mathematics Systems. Available at http://dx.doi.org/10.1007/s10817-009-9138-5.
  32. Gerhard Gentzen (1969): The Collected Papers of Gerhard Gentzen (1934-1938). Edited by Szabo, M. E., North Holland, Amsterdam.
  33. GeoGebra (2008): Dynamische Mathematiksoftware. http://www.geogebra.org. Accessed December 5th, 2011..
  34. Abigail S. Gertner, Cristina Conati & Kurt Vanlehn (1998): Procedural help in Andes: Generating hints using a Bayesian network student. In: Proceedings of the 15th National Conference on Artificial Intelligence. AAAI Press, pp. 106–111. Available at http://www.aaai.org/Conferences/AAAI/aaai98.php.
  35. Jim Grundy & Thomas Långbacka (1997): Recording HOL Proofs in a Structured Browsable Format. In: Michael Johnson: Algebraic Methodology and Software Technology, 6th International Conference, AMAST '97, Sydney, Australia, December 13-17, 1997, Proceedings, Lecture Notes in Computer Science 1349. Springer, pp. 567–571. Available at http://dx.doi.org/10.1007/BFb0000500.
  36. Neil T. Heffernan & Ethan A. Croteau (2004): Web-Based Evaluations Showing Differential Learning for Tutorial Strategies Employed by the Ms. Lindquist Tutor.. In: James C. Lester, Rosa Maria Vicari & Fábio Paraguaçu: Intelligent Tutoring Systems, Lecture Notes in Computer Science 3220. Springer, pp. 491–500. Available at http://dx.doi.org/10.1007/978-3-540-30139-4_46.
  37. Xiaorong Huang (1994): Reconstructing Proofs at the Assertion Level. In: Alan Bundy: Proc. 12th CADE. Springer-Verlag, pp. 738–752.
  38. Xiaorong Huang (1996): Human Oriented Proof Presentation: A Reconstructive Approach. DISKI 112. Infix, Sankt Augustin, Germany.
  39. Cezary Kaliszyk, Freek Wiedijk, Maxim Hendriks & Femke van Raamsdonk (2007): Teaching logic using a state-of-the-art proof assistant. In: H. Geuvers & P. Courtieu: Proc. of the International Workshop on Proof Assistants and Types in Education, pp. 33–48.
  40. John F. Kelley (1984): An iterative design methodology for user-friendly natural language office information applications. ACM Trans. Inf. Syst. 2(1), pp. 26–41. Available at http://dx.doi.org/10.1145/357417.357420.
  41. Kenneth R. Koedinger & Vincent Aleven (2007): Exploring the Assistance Dilemma in Experiments with Cognitive Tutors. Educational Psychology Review 19, pp. 239––264. Available at http://dx.doi.org/10.1007/s10648-007-9049-0.
  42. Kenneth R. Koedinger & John R. Anderson (1993): Reifying implicit planning in geometry: Guidelines for model-based intelligent tutoring system design. In: S. P. Lajoie & S. J. Derry: Computers as cognitive tools. Erlbaum, Hillsdale, NJ, pp. 15–46.
  43. Michael Kohlhase (2006): Mathematical Knowledge Management, 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers. Lecture Notes in Computer Science 3863. Springer. Available at http://dx.doi.org/10.1007/11618027.
  44. Leslie Lamport (1995): How to write a proof. American Mathematical Monthly 102(7), pp. 600–608. Available at http://dx.doi.org/10.2307/2974556.
  45. Chee-Kit Looi, Gordon I. McCalla, Bert Bredeweg & Joost Breuker (2005): Artificial Intelligence in Education - Supporting Learning through Intelligent and Socially Informed Technology, Proceedings of the 12th International Conference on Artificial Intelligence in Education, AIED 2005, July 18-22, 2005, Amsterdam, The Netherlands. Frontiers in Artificial Intelligence and Applications 125. IOS Press.
  46. Noboru Matsuda & Kurt VanLehn (2005): Advanced Geometry Tutor: An intelligent tutor that teaches proof-writing with construction. In: editor = "Looi",, pp. 443–450.
  47. William McCune (2003): Mace4 Reference Manual and Guide. CoRR cs.SC/0310055. Available at http://arxiv.org/abs/cs.SC/0310055.
  48. Bruce M. McLaren, Sung-Joo Lim & Kenneth R. Koedinger (2008): When and how often should worked examples be given to students? New results and a summary of the current state of research. In: Proceedings of the 30th Annual Conference of the Cognitive Science Society. Citeseer, pp. 2176–2181.
  49. Erica Melis, Eric Andrès, Jochen Büdenberger, Adrian Frischauf, George Goguadze, Paul Libbrecht, Martin Pollet & Carsten Ullrich (2001): ActiveMath: A Generic and Adaptive Web-Based Learning Environment. Artifical Intelligence in Education 12(4).
  50. Douglas C. Merrill, Brian J. Reiser, Michael Ranney & J. Gregory Trafton (1992): Effective Tutoring Techniques: A Comparison of Human Tutors and Intelligent Tutoring Systems. The Journal of the Learning Sciences 2(3), pp. 277–305. Available at http://dx.doi.org/10.1207/s15327809jls0203_2.
  51. Dale A. Miller (1984): Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. In: Robert E. Shostak: 7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984, Proceedings, Lecture Notes in Computer Science 170. Springer, pp. 375–393. Available at http://dx.doi.org/10.1007/BFb0047132.
  52. Allen. Newell & Herbert A. Simon (1972): Human Problem Solving. Prentice Hall, Englewood Cliffs.
  53. Jean-François Nicaud, Denis Bouhineau & Thomas Huguet (2002): The Aplusix-Editor: A New Kind of Software for the Learning of Algebra.. In: editor = "Cerri",, pp. 178–187. Available at http://dx.doi.org/10.1007/3-540-47987-2_22.
  54. Stellan Ohlsson (1996): Learning from performance errors. Psychological Review 103, pp. 241–262. Available at http://dx.doi.org/10.1037/0033-295X.103.2.241.
  55. Paulo Ribenboim (1996): The New Book of Prime Number Records. Springer.
  56. Peter J. Robinson & John Staples (1993): Formalizing a Hierarchical Structure of Practical Mathematical Reasoning. J. Log. Comput. 3(1), pp. 47–61. Available at http://dx.doi.org/10.1093/logcom/3.1.47.
  57. Carolyn Penstein Rosé, Johanna D. Moore, Kurt Vanlehn & David Allbritton (2001): A comparative evaluation of socratic versus didactic tutoring. In: Society, University of Edinburgh, pp. 869–874.
  58. Marvin Schiller (2011): Granularity Analysis for Tutoring Mathematical Proofs. AKA Verlag, Heidelberg.
  59. Marvin Schiller, Christoph Benzmüller & Ann Van de Veire (2006): Judging Granularity for Automated Mathematics Teaching. In: LPAR 2006 Short Papers Proceedings, Phnom Pehn, Cambodia.
  60. Wilfried Sieg (2007): The AProS Project: Strategic Thinking & Computational Logic. Logic Journal of the IGPL 15(4), pp. 359–368. Available at http://dx.doi.org/10.1093/jigpal/jzm026.
  61. Wilfried Sieg & Richard Scheines (1994): Computer Environments for Proof Construction. Interactive Learning Environments 4(2), pp. 159–169. Available at http://dx.doi.org/10.1080/1049482940040203.
  62. Daniel Solow (2005): How to read and do proofs. John Wiley and Sons.
  63. Richard Sommer & Gregory Nuckols (2004): A Proof Environment for Teaching Mathematics. Journal of Automated Reasoning 32(3), pp. 227–258. Available at http://dx.doi.org/10.1007/s10817-004-5097-z.
  64. Pramuditha Suraweera & Antonija Mitrovic (2002): KERMIT: A Constraint-Based Tutor for Database Modeling. In: editor = "Cerri",, pp. 377–387. Available at http://dx.doi.org/10.1007/3-540-47987-2_41.
  65. Don Syme (1999): Three Tactic Theorem Proving. In: editor = "Bertot",, pp. 203–220. Available at http://dx.doi.org/10.1007/3-540-48256-3_14.
  66. Donald Syme (1997): DECLARE: a prototype declarative proof system for higher order logic. Technical Report UCAM-CL-TR-416. University of Cambridge.
  67. Jana Trgalova & Hamid Chaachoua (2009): Automatic analysis of proof in a computer-based environment. In: F.-L. Lin, F.-J. Hsieh, G. Hanna & M. de Villiers: Proof and Proving in Mathematics Education, ICMI'19: Proceedings of the 19th International Conference on Mathematics Instruction, Taipei, Taiwan, May 10-15, 2009 1, pp. 226–231.
  68. Dimitra Tsovaltzi (2010): MENON - Automating a Socratic Teaching Model for Mathematical Proofs. Phd thesis. Universität des Saarlandes, Saarbrücken, Germany.
  69. Kurt VanLehn (2006): The Behavior of Tutoring Systems. I. J. Artificial Intelligence in Education 16(3), pp. 227–265. Available at http://iospress.metapress.com/content/al6r85mm7c6qf7dr/.
  70. Kurt VanLehn (2011): The Relative Effectiveness of Human Tutoring, Intelligent Tutoring Systems, and Other Tutoring Systems. Educational Psychologist 46(4), pp. 197–221. Available at http://dx.doi.org/10.1080/00461520.2011.611369.
  71. Kurt VanLehn, Collin Lynch, Kay G. Schulze, Joel A. Shapiro, Robert Shelby, Linwood Taylor, Donald Treacy, Anders Weinstein & Mary Wintersgill (2005): The Andes Physics Tutoring System: Lessons Learned. I. J. Artificial Intelligence in Education 15(3), pp. 147–204. Available at http://iospress.metapress.com/content/4qh80ubfdft0g4yr/.
  72. Markus Wenzel (1999): Isar - A Generic Interpretative Approach to Readable Formal Proof Documents. In: editor = "Bertot",, pp. 167–184. Available at http://dx.doi.org/10.1007/3-540-48256-3_12.
  73. Freek Wiedijk (2004): Formal Proof Sketches. In: Mario Coppo Stefano Berardi & Ferruccio Damiani: Types for Proofs and Programs: Third International Workshop TYPES 2003, LNCS 3085. Springer, Torino, pp. 378–393. Available at http://dx.doi.org/10.1007/978-3-540-24849-1_24.
  74. Magdalena Wolska, Mark Buckley, Helmut Horacek, Ivana Kruijff-Korbayová & Manfred Pinkal (2010): Linguistic Processing in a Mathematics Tutoring System: Cooperative Input Interpretation and Dialogue Modelling. In: Matthew W. Crocker & Jörg Siekmann: Resource-Adaptive Cognitive Processes, Cognitive Technologies. Springer Berlin Heidelberg, pp. 267–289. Available at http://dx.doi.org/10.1007/978-3-540-89408-7_12.
  75. Beverly Park Woolf (2008): Building intelligent interactive tutors: Student-centered strategies for revolutionizing e-learning. Morgan Kaufmann.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org