Section outline

  • VL Formal Modeling (SS 2019)

    Collapse all Expand all

    Wednesday, 15:30-17:00, S2 Z74, Start: March 6, 2019

    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.

  • Organization

    Preliminary Schedule

    • March 6:
      • Introduction to course topics.
    • March 13, March 20, March 27, April 3:
      • Josef Schicho: Mathematical Models in Kinematics and Mechanics
    • April 10, May 8, May 15, May 22:
      • Wolfgang Schreiner: Logical Models of Problems and Computations
    • May 29, June 5, June 12, June 19:
      • Wolfgang Windsteiger: Modeling Problems in Geometry and Discrete Mathematics

    Grading

    Students have to submit 3 positive home assignments to pass the course (if an assignment fails, after the course a substitute is handed out)

  • Mathematical Models in Kinematics and Mechanics

    • Kinematics, as the geometric study of moving rigid bodies in space, and mechanics, where, in addition, the physical laws are relevant, both need an appropriate mathematical/geometric model as a foundation. The model helps to reduce questions to mathematical tasks, and the selection of a model has an influence as to how difficult this task is.
      • Starter: ballistics. How to throw a ball as far as possible.
      • Balancing problems. We study problems of finding equilibria in rigid body dynamics. Many of these problems lead to systems of polynomial equations.
      • Quantum entanglement. Using a simplified model of quantum mechanical model (qubits), we discuss the role of probabilities in quantum mechanics.
    • Assignment 1 (April 29)
    • Balancing File
    • Quantum Mechanics File

  • 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 logical modeling and checking tools such as RISCAL and the TLA Toolbox. In particular, we will consider:
      • Basic problems in computer science, mathematics, and logic.
      • Discrete search and planning problems.
      • Control systems.
    • Theory and Software File
    • Case Studies File
    • RISCAL Models File
    • Assignment 2 (June 5)

  • Modeling 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 techniques from algebra,
    • the Shortest Path Problem, and
    • the Bin Packing Problem.