References

  1. 4ferries. https://fourferries.com/en/home/.
  2. Isac-project. http://www.ist.tugraz.at/isac/History.
  3. Mathtoys. http://mathtoys.org/.
  4. Publications in the ISAC-project. http://www.ist.tugraz.at/isac/Publications_and_Theses.
  5. Slide movie on specifying sub-problems and determining a sequence. http://www.ist.tugraz.at/projects/isac/publ/movie-sub-problems.pdf.
  6. Team of the Isabelle project. https://www21.in.tum.de/.
  7. Team of the ISAC-project. http://www.ist.tugraz.at/isac/Credits.
  8. David Aspinall (2000): Proof General: A Generic Tool for Proof Development. In: Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1785. TACAS, pp. 38–43, doi:10.1007/3-540-46419-0_3.
  9. Franz Baader & Tobias Nipkow (1998): Term Rewriting and All That. Cambridge University Press, Cambridge, doi:10.1017/CBO9781139172752.
  10. Jasmin Christian Blanchette, Lukas Bulwahn & Tobias Nipkow (2011): Automatic Proof and Disproof in Isabelle/HOL, pp. 12–27. Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-642-24364-6_2.
  11. Gabriella Daróczy (2013): Cognitive Aspects of Designing Dialogues in Theorem-Prover Based Mathematics Assistants; Implementation of Error-Patterns Guiding Dialogues in ISAC. ME:CogSci, Vienna, Austria. http://www.ist.tugraz.at/projects/isac/publ/gdaroczy-ma.pdf.
  12. Thomas Maximilian Fink (2001): Benutzerschnittstelle für ein Mathematik-Lernsystem im WWW. University of Technology, Institute for Softwaretechnology, Graz, Austria. http://www.ist.tugraz.at/projects/isac/publ/tf-dipl.pdf.
  13. Kurt Gödel (1986). In: Feferman et al.: Collected Works I. Publications 1929-1936. Oxford University Press, Oxford, pp. 144–195. Translation from: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, 1931.
  14. 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.
  15. Richard Gradischnegg (2004): Eine Java/SML–Schnittstelle für ISAC auf Basis von XML. University of Applied Sciences, Dpt. Software Engineering, Hagenberg, Upper Austria. www.ist.tugraz.at/projects/isac/publ/da-gradischnegg.ps.gz.
  16. Andreas Griesmayer (2003): Architecture and Knowledge-Represenation of the Web-based Math-Learning-System ISAC. University of Technology, Institute for Softwaretechnology, Graz, Austria. www.ist.tugraz.at/projects/isac/publ/da-griesmayer.pdf.
  17. Florian Haftmann (2017): Code generation from Isabelle/HOL theories. Theorem Proving Group at TUM, Munich. Available at http://isabelle.in.tum.de/dist/Isabelle2017/doc/codegen.pdf. Part of the Isabelle distribution.
  18. Mario Hochreiter (2004): Design and Implementation of a Graphical User Interface for the Math-Learning-System ISAC. University of Applied Sciences, Dpt. Software Engineering, Hagenberg, Upper Austria. www.ist.tugraz.at/projects/isac/publ/da-hochreiter.ps.gz.
  19. Lars Hupel & Viktor Kuncak (2016): Translating Scala Programs to Isabelle/HOL, pp. 568–577. Springer International Publishing, Cham, doi:10.1007/978-3-319-40229-1_38.
  20. Natalie Karl (2016): Developing an Inclusive Approach for Representing Mathematical Formulas. Hagenberg University of Applied Sciences, Linz, Austria. http://www.ist.tugraz.at/projects/isac/publ/Masterthesis_NatalieKarl.pdf.
  21. 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.
  22. Franz Kober (2012): Logging of High-Level Steps in a Mechanized Math Assistant. IICM, Graz University of Technology. http://www.ist.tugraz.at/projects/isac/publ/fkober_bakk.pdf.
  23. Martin Korp, Christian Sternagel, Harald Zankl & Aart Middeldorp (2009): Tyrolean Termination Tool 2, pp. 295–304. Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-642-02348-4_21.
  24. Alexander Krauss (2009): Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. Technische Universität München.
  25. 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.
  26. 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.
  27. 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.
  28. Mathias Lehnfeld (2011): Verbindung von 'Computation' und 'Deduction' im ISAC-System. Institut für Computersprachen, Technische Universität Wien. Bakkalaureate project.
  29. Christoph Lüth & Martin Ring (2013): A Web Interface for Isabelle: The Next Generation, pp. 326–329. Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-642-39320-4_22.
  30. Roman E. Maeder (2012): Programming in Mathematica, 3rd edition. Addison-Wesley, Reading, Mass..
  31. 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.
  32. Walther Neuper (2001): Reactive User-Guidance by an Autonomous Engine Doing High-School Math. IICM - Inst. f. Softwaretechnology, Technical University, A-8010 Graz. http://www.ist.tugraz.at/projects/isac/publ/wn-diss.ps.gz.
  33. 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. 9118\p@ plus2\p@ minus4\p@ \z@ plus\p@ 4\p@ plus2\p@ minus2\p@ \defłeftmarginłeftmargini 2.5\p@ plus1.5\p@ minus\p@ 5\p@ plus2\p@ minus5\p@ıtemsep 2.5\p@ plus1.5\p@ minus\p@łeftmarginłeftmargini 4\p@ plus2\p@ minus2\p@ 2\p@ plus\p@ minus\p@ıtemsep +.1667em http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte_Mathematik_und_Fachtheorie.
  34. Walther Neuper (2012): Automated Generation of User Guidance by Combining Computation and Deduction. In: Quaresma & Back, pp. 82–101, doi:10.4204/EPTCS.79.5. http://eptcs.web.cse.unsw.edu.au/paper.cgi?THedu11.5.
  35. Walther Neuper (2014): GCD — A Case Study on Lucas-Interpretation. In: Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM, Coimbra, Portugal. http://ceur-ws.org/Vol-1186/paper-17.pdf.
  36. 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.
  37. Walther Neuper (2017): Formal Abstraction in Engineering Education — Challenges and Technology Support. Acta Didactica Napocensia 10(1), doi:10.24193/adn.10.1.1. With sect.no. http://www.ist.tugraz.at/projects/isac/publ/sys-explain-eng-edu.pdf.
  38. 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. 9118\p@ plus2\p@ minus4\p@ \z@ plus\p@ 4\p@ plus2\p@ minus2\p@ \defłeftmarginłeftmargini 2.5\p@ plus1.5\p@ minus\p@ 5\p@ plus2\p@ minus5\p@ıtemsep 2.5\p@ plus1.5\p@ minus\p@łeftmarginłeftmargini 4\p@ plus2\p@ minus2\p@ 2\p@ plus\p@ minus\p@ıtemsep +.1667em https://www.imst.ac.at/imst-wiki/images/f/f9/683_Kurzfassung_Neuper.pdf.
  39. Walther Neuper & Johannes Reitinger (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. 9118\p@ plus2\p@ minus4\p@ \z@ plus\p@ 4\p@ plus2\p@ minus2\p@ \defłeftmarginłeftmargini 2.5\p@ plus1.5\p@ minus\p@ 5\p@ plus2\p@ minus5\p@ıtemsep 2.5\p@ plus1.5\p@ minus\p@łeftmarginłeftmargini 4\p@ plus2\p@ minus2\p@ 2\p@ plus\p@ minus\p@ıtemsep +.1667em http://imst.uni-klu.ac.at/imst-wiki/index.php/Begreifen_und_Mechanisieren_beim_Algebra-Einstieg.
  40. 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.
  41. 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.
  42. G. E. Pfaff (1985): User Interface Management Systems: Proceedings of the Seeheim Workshop. Springer Verlag, Berlin.
  43. Pedro Quaresma & Ralph-Johan Back (2012): Proceedings First Workshop on CTP Components for Educational Software (THedu'11) 79. Open Publishing Association.
  44. Wolfgang Schreiner, Alexander Brunhuemer & Christoph Fürst (2018): Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models. In: Walther Neuper & Pedro Quaresma: ThEdu'17 Postproceedings, this volume of EPTCS. Open Publishing Association. Johannes Kepler University, Linz.
  45. Christoph Sprenger & Ivano Somaini (2017): Developing Security Protocols by Refinement. Archive of Formal Proofs. http://isa-afp.org/entries/Security_Protocol_Refinement.html, Formal proof development.
  46. ISAC Team (2002): ISAC – User Requirements Document, Software Requirements Document, Architectural Design Document, Software Design Document, Use Cases, Test Cases. Technical Report. Institute for Softwaretechnology, University of Technology. http://www.ist.tugraz.at/projects/isac/publ/isac-docu.pdf.
  47. FH-Design Team (2017): ISAC-Project: User Stories, User Requirements Document, Use Cases Document. http://www.ist.tugraz.at/projects/isac/publ/isac-doc2.pdf.
  48. Josef Urban, Jesse Alama, Piotr Rudnicki & Herman Geuvers (2010): A Wiki for Mizar: Motivation, Considerations, and Initial Prototype, pp. 455–469. Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-642-14128-7_38.
  49. 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. University of Bialystok, pp. 277–298.
  50. Makarius Wenzel (2011): Isabelle as document-oriented proof assistant. In: Proceedings of the 18th Calculemus and 10th international conference on Intelligent computer mathematics, MKM'11. Springer-Verlag, Berlin, Heidelberg, pp. 244–259. Available at http://dl.acm.org/citation.cfm?id=2032713.2032732.
  51. Makarius Wenzel (2012): Isabelle/jEdit — a Prover IDE within the PIDE framework. In: J. Jeuring: Conference on Intelligent Computer Mathematics (CICM 2012), LNAI 7362. Springer, pp. 468–472, doi:10.1007/978-3-642-31374-5_38.
  52. Makarius Wenzel (2014): Asynchronous User Interaction and Tool Integration in Isabelle/PIDE. In: Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, pp. 515–530, doi:10.1007/978-3-319-08970-6_33.
  53. Makarius Wenzel (2017): The Isabelle/Isar Implementation. With contributions by Stefan Berghofer, Florian Haftmann and Larry Paulson.
  54. Makarius Wenzel & Burkhart Wolff (2012): Isabelle/PIDE as Platform for Educational Tools. In: Quaresma & Back, pp. 143–153, doi:10.4204/EPTCS.79.9.
  55. Thomas Zillinger (n.y.): A General Web-Interface of an Assessment-Engine Instantiated for a TP-based Mathematics Assistant. University of Technology, IICM, Graz, Austria. http://www.ist.tugraz.at/projects/isac/publ/tzilling-master.pdf.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org