@article(back-SD-2010,
 author       = {R.-J. Back},
 year         = {2010},
 title        = {Structured derivations: a unified proof style for teaching mathematics},
 journal      = {Formal Aspects of Computing},
 volume       = {22},
 number       = {5},
 pages        = {629--661},
 doi          = {10.1007/s00165-009-0136-5},
)
@book(pl:barend85,
 author       = {H. P. Barendregt},
 year         = {1985},
 title        = {The Lambda Calculus},
 edition      = {second printing},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {103},
 publisher    = {North-Holland},
 address      = {Amsterdam, New York, Oxford},
)
@book(bronstein-integral,
 author       = {Ilja Nikolaevi{\u c} Bronstein and Konstantin Adolfovi{\u c} Semendjajew},
 year         = {1945},
 title        = {Taschenbuch der Mathematik},
 edition      = {23},
 publisher    = {Teubner Verlagsgesellschaft},
 address      = {Leipzig},
 note         = {Translated by Ziegler, Viktor and Wei{\ss}, J\"urgen},
)
@techreport(bb:box,
 author       = {Bruno Buchberger},
 year         = {1992},
 title        = {The White Box / Black Box Principle},
 type         = {Technical Report},
 institution  = {RISC-Linz},
 address      = {Johannes Kepler University, A-4040 Linz},
)
@article(learn-path-09,
 author       = {C. Chen},
 year         = {2009},
 title        = {Ontology-based concept map for planning a personalised learning path},
 journal      = {British Journal of Educational Technology},
 volume       = {40},
 number       = {6},
 pages        = {1028--1058},
 doi          = {10.1111/j.1467-8535.2008.00892.x},
)
@inproceedings(gdaroczy-EP-13,
 author       = {Gabriella Dar\'{o}czy and Walther Neuper},
 year         = {2013},
 title        = {Error-Patterns within ``Next-Step-Guidance'' in TP-based Educational Systems},
 booktitle    = {TP-based Systems and Education},
 volume       = {7},
 publisher    = {eJMT, the Electronic Journal of Mathematics \& Technology},
 pages        = {175--194},
 url          = {https://php.radford.edu/~ejmt/ContentIndex.php#v7n2},
 note         = {Special Issue ``TP-based Systems and Education''},
)
@mastersthesis(MG:thesis,
 author       = {Matthias Goldgruber},
 year         = {2003},
 title        = {{Algebraische Simplifikation mittels Rewriting in \textit{ISAC}}},
 school       = {University of Technology, Institute for Softwaretechnology},
 address      = {Graz, Austria},
 note         = {\url{http://www.ist.tugraz.at/projects/isac/publ/DA-M02-main.ps.gz}},
)
@article(plmms10,
 author       = {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
 year         = {2010},
 title        = {{CTP}-based programming languages~? Considerations about an experimental design},
 journal      = {ACM Communications in Computer Algebra},
 volume       = {44},
 number       = {1/2},
 pages        = {27--41},
 doi          = {10.1145/1838599.1838621},
 note         = {Http://www.ist.tugraz.at/projects/isac/publ/plmms-10.pdf},
)
@incollection(hupel-simp-trace,
 author       = {Lars Hupel},
 year         = {2014},
 title        = {Interactive Simplifier Tracing and Debugging in Isabelle},
 editor       = {StephenM. Watt and JamesH. Davenport and AlanP. Sexton and Petr Sojka and Josef Urban},
 booktitle    = {Intelligent Computer Mathematics},
 series       = {Lecture Notes in Computer Science},
 volume       = {8543},
 publisher    = {Springer International Publishing},
 pages        = {328--343},
 doi          = {10.1007/978-3-319-08434-3_24},
)
@mastersthesis(mkienl-bakk,
 author       = {Markus Kienleitner},
 year         = {2012},
 title        = {Towards ``NextStep Userguidance'' in a Mechanized Math Assistant},
 school       = {IICM, Graz University of Technology},
 note         = {\url{http://www.ist.tugraz.at/projects/isac/publ/mkienl_bakk.pdf}},
)
@article(stellungn-dmv-gdm-mnu,
 author       = {W. Kopef and M R\"ockner and A. Eichler and G. Heckmann},
 year         = {2017},
 title        = {Zur aktuellen {D}iskussion \"uber die {Q}ualit\"at des {M}athematikunterrichts},
 journal      = {Mitteilungen der Deutschen Mathematiker-Vereinigung},
 volume       = {25},
 number       = {1},
 pages        = {6--7},
 doi          = {10.1515/dmvm-2017-0005},
 note         = {\url{http://www.mathematik-schule-hochschule.de/images/Stellungnahmen/pdf/Stellungnahme-DMVGDMMNU-2017.pdf}},
)
@inproceedings(krauss,
 author       = {Alexander Krauss},
 year         = {2006},
 title        = {Partial Recursive Functions in Higher-Order Logic},
 editor       = {Ulrich Furbach and Natarajan Shankar},
 booktitle    = {IJCAR},
 series       = {Lecture Notes in Computer Science},
 volume       = {4130},
 publisher    = {Springer},
 pages        = {589--603},
 doi          = {10.1007/11814771\_48},
)
@mastersthesis(AK04:thesis,
 author       = {Alan Krempler},
 year         = {2005},
 title        = {Architectural Design for Integrating an Interactive Dialogguide into a Mathematical Tutoring System},
 school       = {University of Technology, Institute for Softwaretechnology},
 address      = {Graz, Austria},
 note         = {\url{http://www.ist.tugraz.at/projects/isac/publ/da-krempler.pdf}},
)
@inproceedings(kremp.np:assess,
 author       = {Alan Krempler and Walther Neuper},
 year         = {2008},
 title        = {Formative Assessment for User Guidance in Single Stepping Systems},
 editor       = {Michael E. Aucher},
 booktitle    = {Interactive Computer Aided Learning, Proceedings of ICL08},
 address      = {Villach, Austria},
 note         = {\url{http://www.ist.tugraz.at/projects/isac/publ/icl08.pdf}},
)
@inproceedings(wn:proto-sys,
 author       = {Alan Krempler and Walther Neuper},
 year         = {2018},
 title        = {Prototyping ``Systems that Explain Themselves'' for Education},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {{\rm Proceedings 6th International Workshop on} Theorem proving components for Educational software, {\rm Gothenburg, Sweden, 6 Aug 2017}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {267},
 publisher    = {Open Publishing Association},
 pages        = {89--107},
 doi          = {10.4204/EPTCS.267.6},
)
@mastersthesis(richard:da,
 author       = {Richard Lang},
 year         = {2003},
 title        = {{Elementare Gleichungen der Mittelschulmathematik in der \textit{ISAC}Wissensbasis}},
 school       = {University of Technology, Institute of Software Technology},
 address      = {Graz, Austria},
 note         = {\url{http://www.ist.tugraz.at/projects/isac/publ/da-rlang.ps.gz}},
)
@mastersthesis(mmahringer,
 author       = {Marco Mahringer},
 year         = {2018},
 title        = {Formula Editors for {TP}-based Systems. State of the Art and Prototype Implementation in \textit{ISAC}},
 school       = {University of Applied Sciences},
 address      = {Hagenberg, Austria},
 note         = {\url{http://www.ist.tugraz.at/projects/isac/publ/mmahringer-master.pdf}},
)
@book(malle93:algebra,
 author       = {G\"unther Malle},
 year         = {1993},
 title        = {Didaktische {P}robleme der elementaren {A}lgebra},
 publisher    = {Vieweg},
 doi          = {10.1007/978-3-322-89561-5},
)
@techreport(imst-htl06,
 author       = {Walther Neuper},
 year         = {2006},
 title        = {{Angewandte Mathematik und Fachtheorie}},
 type         = {Technical Report},
 number       = {357},
 institution  = {IMST -- Innovationen Machen Schulen Top!},
 address      = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
 note         = {\url{http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte\_Mathematik\_und\_Fachtheorie}},
)
@inproceedings(wn:lucas-interp-12,
 author       = {Walther Neuper},
 year         = {2012},
 title        = {Automated Generation of User Guidance by Combining Computation and Deduction},
 editor       = {Pedro Quaresma and Ralph-Johan Back},
 booktitle    = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {79},
 publisher    = {Open Publishing Association},
 pages        = {82--101},
 doi          = {10.4204/EPTCS.79.5},
 note         = {\url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?THedu11.5}},
)
@inproceedings(thedu16:lucin-user-view,
 author       = {Walther Neuper},
 year         = {2016},
 title        = {Lucas-Interpretation from Users' Perspective},
 booktitle    = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics},
 address      = {Bialystok, Poland},
 pages        = {83--89},
 note         = {\url{http://cicm-conference.org/2016/ceur-ws/CICM2016-WIP.pdf}},
)
@inproceedings(wn:lucin-thedu18,
 author       = {Walther Neuper},
 year         = {2018},
 title        = {Lucas-Interpretation from Programmers' Perspective},
 note         = {Abstract for ThEdu'18 \url{http://www.ist.tugraz.at/projects/isac/publ/lucin-prog-view.pdf}},
)
@inproceedings(wn:cme-ei-18,
 author       = {Walther Neuper},
 year         = {2018},
 title        = {Mechanical Explanation in ``Systems that explain themselves''},
 editor       = {Osman Hasan},
 booktitle    = {Workshop Papers at 11th Conference on Intelligent Computer Mathematics CICM 2018},
 publisher    = {Conference on Intelligent Computer Mathematics CICM},
 address      = {Hagenberg, Austria},
 note         = {\url{https://www.cicm-conference.org/2018/infproc/paper1.pdf}},
)
@techreport(imst-htl07,
 author       = {Walther Neuper and Christian D\"urnsteiner},
 year         = {2007},
 title        = {{Angewandte Mathematik und Fachtheorie mithilfe adaptierter Basis-Software}},
 type         = {Technical Report},
 number       = {683},
 institution  = {IMST -- Innovationen Machen Schulen Top!},
 address      = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
 note         = {\url{https://www.imst.ac.at/imst-wiki/images/f/f9/683_Kurzfassung_Neuper.pdf}},
)
@techreport(imst-hpts08,
 author       = {Walther Neuper and Johannes Reitinger and Angelika Gr\"undlinger},
 year         = {2008},
 title        = {{Begreifen und Mechanisieren beim Algebra Einstieg}},
 type         = {Technical Report},
 number       = {1063},
 institution  = {IMST -- Innovationen Machen Schulen Top!},
 address      = {University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15},
 note         = {\url{https://www.imst.ac.at/imst-wiki/images/9/9d/1063_Langfassung_Reitinger.pdf}},
)
@article(sys-of-sys-15,
 author       = {Claus Ballegaard Nielsen and Peter Gorm Larsen and John Fitzgerald and Jim Woodcock and Jan Peleska},
 year         = {2015},
 title        = {Systems of Systems Engineering: Basic Concepts, Model-Based Techniques, and Research Directions},
 journal      = {ACM Comput. Surv.},
 volume       = {48},
 number       = {2},
 pages        = {18:1--18:41},
 doi          = {10.1145/2794381},
)
@book(Isa-tutor08,
 author       = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
 year         = {2008},
 title        = {Isabelle/HOL, a proof assistant for high-order logic},
 publisher    = {Springer Verlag},
)
@incollection(PISA-math-2015,
 author       = {{OECD}},
 year         = {2017},
 title        = {{PISA} 2015 Mathematics Framework},
 booktitle    = {PISA 2015 Assessment and Analytical Framework: Science, Reading, Mathematic, Financial Literacy and Collaborative Problem Solving},
 publisher    = {OECD Publishing},
 address      = {Paris},
 doi          = {10.1787/9789264281820-5-en},
 note         = {\url{https://www.oecd-ilibrary.org/docserver/9789264281820-5-en.pd} [Retrieved 23.Apr.2018]},
)
@book(Gentzen:nat-deduct,
 author       = {John Riser},
 year         = {1969},
 title        = {The collected papers of Gerhard Gentzen},
 series       = {Studies in logic and the foundations of mathematics},
 publisher    = {North-Holland Publ. Co.},
 address      = {Amsterdam},
 doi          = {10.1017/S0022481200092604},
)
@inproceedings(DBLP:conf/mkm/Schreiner18,
 author       = {Wolfgang Schreiner},
 year         = {2018},
 title        = {Validating Mathematical Theorems and Algorithms with {RISCAL}},
 editor       = {Osman Hasan},
 booktitle    = {Intelligent Computer Mathematics - 11th International Conference, {CICM} 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings},
 organization = {CICM Conference on Intelligent Computer Mathematics},
 publisher    = {CEUR-WS},
 address      = {\url{ceur-ws.org/}},
 pages        = {248--254},
 doi          = {10.1007/978-3-319-96812-4\_21},
)
@inproceedings(DBLP:journals/corr/Wenzel14,
 author       = {Makarius Wenzel},
 year         = {2014},
 title        = {System description: {Isabelle/jEdit} in 2014},
 editor       = {Christoph Benzm\"uller and Bruno Woltzenlogel Paleo},
 booktitle    = {Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, {UITP} 2014, Vienna, Austria, 17th July 2014.},
 address      = {Vienna, Austria},
 pages        = {84--94},
 doi          = {10.4204/EPTCS.167.10},
)
@inproceedings(wenzel:isar,
 author       = {Markus Wenzel},
 year         = {1999},
 title        = {Isar - a Generic Interpretative Approach to Readable Formal Proof Documents},
 editor       = {G. Dowek and A. Hirschowitz and C. Paulin and L. Thery},
 booktitle    = {Theorem Proving in Higher Order Logics},
 series       = {LNCS 1690},
 organization = {12th International Conference TPHOLs'99},
 publisher    = {Springer},
 doi          = {10.1007/BFb0030541},
)