References

  1. R.-J. Back (2010): Structured derivations: a unified proof style for teaching mathematics. Formal Aspects of Computing 22(5), pp. 629–661, doi:10.1007/s00165-009-0136-5.
  2. H. P. Barendregt (1985): The Lambda Calculus, second printing edition, Studies in Logic and the Foundations of Mathematics 103. North-Holland, Amsterdam, New York, Oxford.
  3. Ilja Nikolaevic Bronstein & Konstantin Adolfovic Semendjajew (1945): Taschenbuch der Mathematik, 23 edition. Teubner Verlagsgesellschaft, Leipzig. Translated by Ziegler, Viktor and Weiß, Jürgen.
  4. Bruno Buchberger (1992): The White Box / Black Box Principle. Technical Report. RISC-Linz, Johannes Kepler University, A-4040 Linz.
  5. C. Chen (2009): Ontology-based concept map for planning a personalised learning path. British Journal of Educational Technology 40(6), pp. 1028–1058, doi:10.1111/j.1467-8535.2008.00892.x.
  6. Gabriella Daróczy & Walther Neuper (2013): Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems. In: TP-based Systems and Education 7. eJMT, the Electronic Journal of Mathematics & Technology, pp. 175–194. Available at https://php.radford.edu/~ejmt/ContentIndex.php#v7n2. Special Issue ``TP-based Systems and Education''.
  7. Matthias Goldgruber (2003): Algebraische Simplifikation mittels Rewriting in ISAC. University of Technology, Institute for Softwaretechnology, Graz, Austria. http://www.ist.tugraz.at/projects/isac/publ/DA-M02-main.ps.gz.
  8. Florian Haftmann, Cezary Kaliszyk & Walther Neuper (2010): CTP-based programming languages ? Considerations about an experimental design. ACM Communications in Computer Algebra 44(1/2), pp. 27–41, doi:10.1145/1838599.1838621. Http://www.ist.tugraz.at/projects/isac/publ/plmms-10.pdf.
  9. Lars Hupel (2014): Interactive Simplifier Tracing and Debugging in Isabelle. In: StephenM. Watt, JamesH. Davenport, AlanP. Sexton, Petr Sojka & Josef Urban: Intelligent Computer Mathematics, Lecture Notes in Computer Science 8543. Springer International Publishing, pp. 328–343, doi:10.1007/978-3-319-08434-3_24.
  10. Markus Kienleitner (2012): Towards ``NextStep Userguidance'' in a Mechanized Math Assistant. IICM, Graz University of Technology. http://www.ist.tugraz.at/projects/isac/publ/mkienl_bakk.pdf.
  11. W. Kopef, M Röckner, A. Eichler & G. Heckmann (2017): Zur aktuellen Diskussion über die Qualität des Mathematikunterrichts. Mitteilungen der Deutschen Mathematiker-Vereinigung 25(1), pp. 6–7, doi:10.1515/dmvm-2017-0005. http://www.mathematik-schule-hochschule.de/images/Stellungnahmen/pdf/Stellungnahme-DMVGDMMNU-2017.pdf.
  12. Alexander Krauss (2006): Partial Recursive Functions in Higher-Order Logic. In: Ulrich Furbach & Natarajan Shankar: IJCAR, Lecture Notes in Computer Science 4130. Springer, pp. 589–603, doi:10.1007/11814771_48.
  13. Alan Krempler (2005): Architectural Design for Integrating an Interactive Dialogguide into a Mathematical Tutoring System. University of Technology, Institute for Softwaretechnology, Graz, Austria. http://www.ist.tugraz.at/projects/isac/publ/da-krempler.pdf.
  14. Alan Krempler & Walther Neuper (2008): Formative Assessment for User Guidance in Single Stepping Systems. In: Michael E. Aucher: Interactive Computer Aided Learning, Proceedings of ICL08, Villach, Austria. http://www.ist.tugraz.at/projects/isac/publ/icl08.pdf.
  15. Alan Krempler & Walther Neuper (2018): Prototyping ``Systems that Explain Themselves'' for Education. In: Pedro Quaresma & Walther Neuper: Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017, Electronic Proceedings in Theoretical Computer Science 267. Open Publishing Association, pp. 89–107, doi:10.4204/EPTCS.267.6.
  16. Richard Lang (2003): Elementare Gleichungen der Mittelschulmathematik in der ISACWissensbasis. University of Technology, Institute of Software Technology, Graz, Austria. http://www.ist.tugraz.at/projects/isac/publ/da-rlang.ps.gz.
  17. Marco Mahringer (2018): Formula Editors for TP-based Systems. State of the Art and Prototype Implementation in ISAC. University of Applied Sciences, Hagenberg, Austria. http://www.ist.tugraz.at/projects/isac/publ/mmahringer-master.pdf.
  18. Günther Malle (1993): Didaktische Probleme der elementaren Algebra. Vieweg, doi:10.1007/978-3-322-89561-5.
  19. Walther Neuper (2006): Angewandte Mathematik und Fachtheorie. Technical Report 357. IMST – Innovationen Machen Schulen Top!, University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15. http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte_Mathematik_und_Fachtheorie.
  20. Walther Neuper (2012): Automated Generation of User Guidance by Combining Computation and Deduction. In: Pedro Quaresma & Ralph-Johan Back: Electronic Proceedings in Theoretical Computer Science 79. Open Publishing Association, pp. 82–101, doi:10.4204/EPTCS.79.5. http://eptcs.web.cse.unsw.edu.au/paper.cgi?THedu11.5.
  21. Walther Neuper (2016): Lucas-Interpretation from Users' Perspective. In: Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics, Bialystok, Poland, pp. 83–89. http://cicm-conference.org/2016/ceur-ws/CICM2016-WIP.pdf.
  22. Walther Neuper (2018): Lucas-Interpretation from Programmers' Perspective. Abstract for ThEdu'18 http://www.ist.tugraz.at/projects/isac/publ/lucin-prog-view.pdf.
  23. Walther Neuper (2018): Mechanical Explanation in ``Systems that explain themselves''. In: Osman Hasan: Workshop Papers at 11th Conference on Intelligent Computer Mathematics CICM 2018. Conference on Intelligent Computer Mathematics CICM, Hagenberg, Austria. https://www.cicm-conference.org/2018/infproc/paper1.pdf.
  24. Walther Neuper & Christian Dürnsteiner (2007): Angewandte Mathematik und Fachtheorie mithilfe adaptierter Basis-Software. Technical Report 683. IMST – Innovationen Machen Schulen Top!, University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15. https://www.imst.ac.at/imst-wiki/images/f/f9/683_Kurzfassung_Neuper.pdf.
  25. Walther Neuper, Johannes Reitinger & Angelika Gründlinger (2008): Begreifen und Mechanisieren beim Algebra Einstieg. Technical Report 1063. IMST – Innovationen Machen Schulen Top!, University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15. https://www.imst.ac.at/imst-wiki/images/9/9d/1063_Langfassung_Reitinger.pdf.
  26. Claus Ballegaard Nielsen, Peter Gorm Larsen, John Fitzgerald, Jim Woodcock & Jan Peleska (2015): Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions. ACM Comput. Surv. 48(2), pp. 18:1–18:41, doi:10.1145/2794381.
  27. Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2008): Isabelle/HOL, a proof assistant for high-order logic. Springer Verlag.
  28. OECD (2017): PISA 2015 Mathematics Framework. In: PISA 2015 Assessment and Analytical Framework: Science, Reading, Mathematic, Financial Literacy and Collaborative Problem Solving. OECD Publishing, Paris, doi:10.1787/9789264281820-5-en. https://www.oecd-ilibrary.org/docserver/9789264281820-5-en.pd [Retrieved 23.Apr.2018].
  29. John Riser (1969): The collected papers of Gerhard Gentzen. Studies in logic and the foundations of mathematics. North-Holland Publ. Co., Amsterdam, doi:10.1017/S0022481200092604.
  30. Wolfgang Schreiner (2018): Validating Mathematical Theorems and Algorithms with RISCAL. In: Osman Hasan: Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings. CICM Conference on Intelligent Computer Mathematics. CEUR-WS, ceur-ws.org/, pp. 248–254, doi:10.1007/978-3-319-96812-4_21.
  31. Makarius Wenzel (2014): System description: Isabelle/jEdit in 2014. In: Christoph Benzmüller & Bruno Woltzenlogel Paleo: Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, UITP 2014, Vienna, Austria, 17th July 2014., Vienna, Austria, pp. 84–94, doi:10.4204/EPTCS.167.10.
  32. Markus Wenzel (1999): Isar - a Generic Interpretative Approach to Readable Formal Proof Documents. In: G. Dowek, A. Hirschowitz, C. Paulin & L. Thery: Theorem Proving in Higher Order Logics, LNCS 1690. 12th International Conference TPHOLs'99. Springer, doi:10.1007/BFb0030541.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org