References

  1. Mauricio Ayala-Rincón & Thaynara Arielly de Lima (2020): Teaching Interactive Proofs to Mathematicians. In: Pedro Quaresma, Walther Neuper & João Marcos: Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, Paris, France, 29th June 2020, Electronic Proceedings in Theoretical Computer Science 328. Open Publishing Association, pp. 1–17, doi:10.4204/EPTCS.328.1.
  2. Ralph-Johan Back & Joakim von Wright (2006): Mathematics with a Little Bit of Logic: Structured Derivations in High-School Mathematics. Manuscript.
  3. Sidney Bender, Monica Haurilet, Alina Roitberg & Rainer Stiefelhagen (2019): Learning Fine-Grained Image Representations for Mathematical Expression Recognition. In: 2019 International Conference on Document Analysis and Recognition Workshops (ICDARW) 1, pp. 56–61, doi:10.1109/ICDARW.2019.00015.
  4. Dines Bjørner & Klaus Havelund (2014): 40 Years of Formal Methods - Some Obstacles and Some Possibilities?. In: FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, pp. 42–61, doi:10.1007/978-3-319-06410-9_4.
  5. Merlin Carl (2020): Number Theory and Axiomatic Geometry in the Diproche System. In: Pedro Quaresma, Walther Neuper & João Marcos: Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, Paris, France, 29th June 2020, Electronic Proceedings in Theoretical Computer Science 328. Open Publishing Association, pp. 56–78, doi:10.4204/EPTCS.328.4.
  6. David M. Cerna, Rafael P.D. Kiesel & Alexandra Dzhiganskaya (2020): A Mobile Application for Self-Guided Study of Formal Reasoning. In: Pedro Quaresma, Walther Neuper & João Marcos: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, Natal, Brazil, 25th August 2019, Electronic Proceedings in Theoretical Computer Science 313. Open Publishing Association, pp. 35–53, doi:10.4204/EPTCS.313.3.
  7. Gabriella Daróczy & Walther Neuper (2013): Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems. In: eJMT, the Electronic Journal of Mathematics & Technology 7, pp. 175–194. Available at https://php.radford.edu/~ejmt/ContentIndex.php#v7n2. Special Issue ``TP-based Systems and Education''.
  8. William M. Farmer (2000): A proposal for the development of an interactive mathematics laboratory for mathematics eduction. In: CADE-17 Workshop on Deduction Systems for Mathematics Education, pp. 20–25.
  9. Asta Halkjær From, Jørgen Villadsen & Patrick Blackburn (2020): Isabelle/HOL as a Meta-Language for Teaching Logic. In: Pedro Quaresma, Walther Neuper & João Marcos: Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, Paris, France, 29th June 2020, Electronic Proceedings in Theoretical Computer Science 328. Open Publishing Association, pp. 18–34, doi:10.4204/EPTCS.328.2.
  10. David Gries (1981): The science of programming. Texts and monographs in computer science. Springer-Verlag, doi:10.1007/978-1-4612-5983-1.
  11. Gila Hanna & Michael de Villiers (2012): Proof and Proving in Mathematics Education. The 19th ICMI Study. New ICMI Study Series 15. Springer.
  12. Antonia Huertas (2011): Ten Years of Computer-based Tutors for Teaching Logic 2000-2010: Lessons Learned. In: Proceedings of the Third International Congress Conference on Tools for Teaching Logic (TICTTL’11). Springer-Verlag, Berlin, Heidelberg, pp. 131–140, doi:10.1093/jigpal/jzm019.
  13. P. Jitngernmadan & K. Miesenberger (2015): A Comparative Study on Java Technologies for Focus and Cursor Handling in Accessible Dynamic Interactions. In: C. Sikne Lanyi: Proceedings of AAATE. IOS Press, Amsterdam, Budapest.
  14. P. Jitngernmadan & K. Miesenberger (2017): Extraction Methodology of Implicit Didactics in Math Schoolbooks for the Blind. In: P. Cudd & L. De Witte: Proceedings AAATE Conference 2017. Harnessing the Power of Technology to Improve Lives. IOS Press, Amsterdam.
  15. P. Jitngernmadan, A. Petz, B. Stöger & K. Miesenberger (2016): Analysis of Implicit Didactics in Math Schoolbooks for Interactive Non-visual User Interface Development. In: K. Miesenberger, C. Bühler & P. Penaz: Computers Helping People with Special Needs, 15th International Conference, ICCHP 2016. Springer Heidelberg, Linz Austria, doi:10.1007/978-3-319-41264-1_3.
  16. P. Jitngernmadan, B. Stöger, A Petz & K. Miesenberger (2017): IDMILE: An interactive didactic math inclusion learning environment for blind students. Technology and Disability 29(1-2), pp. 47–61, doi:10.3233/TAD-170173.
  17. Prajaks Jitngernmadan (2017): A Framework of Support Functionalities for Multimodal Interface Design for Mathematic Working Environment. Johannes Kepler University Linz, Austria.
  18. Natalie Karl (2016): Developing an Inclusive Approach for Representing Mathematical Formulas. Hagenberg University of Applied Sciences, Linz, Austria. https://static.miraheze.org/isacwiki/0/02/Masterthesis_NatalieKarl.pdf.
  19. Boris Koichu & Alon Pinto (2019): The Secondary-Tertiary Transition in Mathematics. What are our current challenges and what can we do about them?. EMS Newsletter, pp. 34–35, doi:10.4171/NEWS.
  20. 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.
  21. 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.
  22. Peter Lucas (1978): On the Formalization of Programming Languages: Early History and Main Approaches. In: D. Bjørner & C. B. Jones: The Vienna Development Method: The Meta-Language, LNCS 16. Springer, doi:10.1007/3-540-08766-4_8.
  23. Peter Lucas & Kurt Walk (1970): On the Formal Description of PL/I. Annual Review in Automatic Programming 6. Pergamon Press, Oxford.
  24. Marco Mahringer (2018): Formula Editors for TP-based Systems. State of the Art and Prototype Implementation in ISAC. University of Applied Sciences, Hagenberg, Austria. https://static.miraheze.org/isacwiki/d/d7/Mmahringer-master.pdf.
  25. Erica Melis & Jörg Siekmann (2004): An Intelligent Tutoring System for Mathematics. In: L. Rutkowski, J. Siekmann, R. Tadeusiewicz & L.A. Zadeh: Seventh International Conference ’Artificial Intelligence and Soft Computing’ (ICAISC), LNAI 3070,. Springer-Verlag, pp. 91–101, doi:10.1007/978-3-540-24844-6_12.
  26. 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.
  27. Walther Neuper (2019): Technologies for ``Complete, Transparent & Interactive Models of Math'' in Education. In: Pedro Quaresma & Walther Neuper: Proceedings 7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 july 2018, Electronic Proceedings in Theoretical Computer Science 290. Open Publishing Association, pp. 76–95, doi:10.4204/EPTCS.290.6.
  28. Walther Neuper (2020): Lucas-Interpretation on Isabelle's Functions. In: Pedro Quaresma, Walther Neuper & João Marcos: Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, Paris, France, 29th June 2020, Electronic Proceedings in Theoretical Computer Science 328. Open Publishing Association, pp. 79–95, doi:10.4204/EPTCS.328.5.
  29. 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.
  30. 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.
  31. 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.
  32. Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002): Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer, doi:10.1007/3-540-45949-9.
  33. 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.
  34. Lawrence C. Paulson & Jasmin C. Blanchette (2010): Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. In: Schulz S. Sutcliffe G., Ternovska E.: IWIL 2010. Springer. http://people.mpi-inf.mpg.de/~jblanche/iwil2010-sledgehammer.pdf.
  35. Lawrence C. Paulson, Tobias Nipkow & Makarius Wenzel (2019): From LCF to Isabelle/HOL. Formal Aspects of Computing 31, pp. 675–698, doi:10.1007/s00165-019-00492-1. Springer, London.
  36. Wolfgang Schreiner, Alexander Brunhuemer & Christoph Fürst (2018): Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models. In: Pedro Quaresma & Walther Neuper: Post-Proceedings ThEdu'17, Electronic Proceedings in Theoretical Computer Science (EPTCS) 267. Open Publishing Association, pp. 120–139, doi:10.4204/EPTCS.267.8.
  37. M. Suzuki, F. Tamari, R. Fukuda, S. Uchida & T. Kanahori (2003): Infty ? an integrated OCR system for mathematical documents. In: Proc. ACA Symposium on Document Engineering, pp. 95–104.
  38. M. Suzuki & K. Yamaguchi (2020): On Automatic Conversion from e-Born PDF into Accessible EPUB3 and Audio-Embedded HTML5. In: Proc. the 17th International Conference on Computers Helping People with Special Needs (ICCHP 2020), LNCS 12376. Springer, pp. 410–416, doi:10.1007/978-3-030-58796-3_48.
  39. Makarius Wenzel (2007): Isabelle/Isar — a generic framework for human-readable proof documents. In: R. Matuszewski & A. Zalewska: From Insight to Proof — Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric 10(23). University of Białystok. Available at https://www21.in.tum.de/~wenzelm/papers/isar-framework.pdf.
  40. Makarius Wenzel (2019): Interaction with Formal Mathematical Documents in Isabelle/PIDE. In: Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase & Claudio Sacerdoti Coen: Intelligent Computer Mathematics (CICM 2019) 11617. Springer, doi:10.48550/arXiv.1905.01735.
  41. Makarius Wenzel (2021): The Isabelle System Manual. Available at https://isabelle.in.tum.de/dist/Isabelle2021/doc/system.pdf. Contained in the Isabelle distribution.
  42. W.Neuper, B.Stöger & M.Wenzel (2022): Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode. Isabelle Workshop 2022 https://sketis.net/isabelle/isabelle-workshop-2022. Accessed: 202-10-13.
  43. K. Yamaguchi & M. Suzuki (2019): An accessible STEM editor customizable for various local languages. Journal of Enabling Technologies 13(4), pp. 240–250, doi:10.1108/JET-12-2018-0064.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org