Lecture notes

During the development of the $\mmath$-project, the redesign of beginner lectures on analysis and modeling in terms of emphasizing formal aspects played a very important role. The resulting lecture notes integrate parts of the $\mmath$-language: Definitions of concepts are written as models and proofs are presented in a way that the $\mmath$-actions and their semantics become explicitly visible.

The syntax used in the LaTeX-documents, however, is not identical to the $\mmath$ surface syntax. In the initial chapters of the analysis notes, a syntax very close to the $\mmath$ one is used for formulating proofs, modified by some formatting for better readability and interrupted by informal paragraphs for explanations. These proofs could easily be modified to serve as input for the proof checker. In the later chapters the syntax becomes more informal without losing focus on the semantics. While in the beginning, proofs are stated in detail and could be used as an input for the proof checker, the level of detail drops in later chapters, leaving the task of filling the emerging gaps to the students.

In the modeling course, focus is put on the modeling process itself rather than on proofs. For the purpose of providing a clearly defined and standardized way of writing down models, the $\mmath$-syntax for models is utilized, since it is designed to highlight the important parts of a mathematical model. Throughout the lecture the $\mmath$-syntax is used to state models, again interrupted by informal explanatory parts.

The latest versions of the lecture notes (in German) can be found here. Since the notes were written parallel to the language development, a slight drift in the syntax can be observed.