Topic outline
VL Formal Modeling (WS 2022)
326.006, Wednesday, 15:30-17:00, Room: S2 Z74 Start: October 5, 2022
We discuss the formal modeling of mathematical problems that are amenable to algorithms and software from symbolic computation; the models are based on the language of algebra and logic. In this lecture, we discuss particular examples from various application domains. In the accompanying proseminar students are expected to model selected problems and demonstrate their results in the form of small papers and presentations.
As an extra service, some course units may be live-streamed and recorded via the following Zoom Meeting (but no guarantee is given with respect to completeness and quality of the streams, the basic format is on-site, not hybrid):
Zoom Meeting
https://jku.zoom.us/j/95922982482?pwd=ejFPeVEyekswZFRRQ0h4MWlzRlNpdz09
Meeting-ID: 995 2030 2042 Password: ..modelingOrganization
Preliminary Schedule
- October 5:
- Introduction to course topics.
- October 12, October 19, December 7, December 14:
- Wolfgang Schreiner: Logical Models of Problems and Computations
- November 9, November 16, January 11, January 18:
- Wolfgang Windsteiger: Modeling Problems in Geometry and Discrete Mathematics
- November 16 (17:15-18:45), November 23 (17:15-18:45), November 30 (17:15-18:45):
- Carsten Schneider: Symbolic Summation and the Modeling of Sequences
GradingStudents have to submit 3 positive home assignments to pass the course (if an assignment fails, after the course a substitute is handed out)
- October 5:
Logical Models of Problems and Computations
- We discuss the logical specification of computational problems and the logical modeling of computational systems. Problems are analyzed with respect to various criteria (adequacy, satisfiability, non-triviality, uniqueness of results), systems are analyzed with respect to safety properties. For this we apply the mathemtical model checker RISCAL. In particular, we will consider:
- Basic problems in computer science, mathematics, and logic.
- Discrete search and planning problems.
- Control systems.
- Basic problems in computer science, mathematics, and logic.
Password is handed out in class
Symbolic Summation and the modeling of sequences
In this part of the lecture we will deal with the challenge to model sequences (infinite objects) by using computer algebra technologies.
Special focus will be put on
- modeling sequences tailored for the user in the setting of term algebras;
- modeling sequences in formal difference rings tailored for the computer ;
- connecting the two worlds to extract interesting properties for the user.
The lecture will be enhanced stepwise and the topics will be summarized within the lecture notes that can be found here. In addition, there are slides and a Matheamtica Notebook given here that supplements the lecture.The corresponding homeworks will be explained in the lecture. The precise specification can be found here.- Lecture 1: 16. November 2022
Symbolic summation (a short introduction) - Lecture 2: 23. November 2022
Modeling of sequences with a term algebra (the user interface) - Lecture 3: 30. November 2022
Modeling of sequences in difference rings (computer algebra)
Modelling Problems in Geometry and Discrete Mathematics
We discuss geometric problems and problems that can be modelled in the language of graph theory and in the language of combinatorial optimization. After modelling the problems appropriately we discuss general and special solution techniques and algorithms that can be applied to these problems. Problems discussed will cover
- proving geometrical statements using algebraic techniques,
- the Shortest Path Problem, and
- the Bin Packing Problem.
Mode for this part of the lecture
This part of the lecture will be held in the "flipped classroom"-mode, the amount of work is split into 50% video study + 50% presence in the lecture (via Zoom in this case). This results in two presence lectures (instead of four), the respective videos need to be studied in advance. If questions arise during the video study, then ask in the "Discussion"-forum in Moodle or send email to the lecturer personally. With this preparation you come to the lecture (and know already the basics from the videos, the lecture notes, and the slides). In the lecture, you will see (more) examples, you can ask questions, discuss problems, etc. You will notice that certain parts of the slides are not part of the videos or the videos of these parts will only be available after the lecture. This indicates material that is planned to be discussed in the respective lecture.Lecture November 16
Videos: Modelling and Proving in Geometry
Videos: Modelling in Graph Theory (part I)
Lecture January 18
Videos: Modelling in Graph Theory (part II)
Videos: Modelling in Discrete Optimization
- proving geometrical statements using algebraic techniques,