VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.
Computer-Supported Modeling and Reasoning
Last Updated: 2026-02-05 15:07:02
Abstract
This course introduces into higher-order logic and typed set theory, and teaches to use it as a practical tool. Mathematical theories are built in a consistent way and formal proofs are engineered such that they can be machine checked. The course is centered around the theorem prover Isabelle/HOL.
Objective
The aim of this course is to show how to use higher-order logic and typed set theory as a practical tool. Participants will learn how to use a theorem prover to build mathematical theories and carry out machine-checked proofs. The theories are problems in mathematics and computer science, such as formal language semantics, system models and program verifications.
Content
The aim of this course is to show how to use higher-order logic and typed set theory as a practical tool. Participants will learn how to use a theorem prover to build mathematical theories and carry out machine-checked proofs. The theories can be about mathematical problems as well as artifacts in computer science like formal language semantics, system models and program verifications. The course is intended for students of computer science, mathematics, and related disciplines, who are interested in rigorous techniques for formal modeling and reasoning. A basic knowledge of mathematical logic is recommended for this course.
Resources
Lecture Notes
For each topic covered in the course, we will make the course material and supplementary material online,
Literature
D. van Dalen: Logic and Structure. Springer-Verlag, 1980. An introductory textbook on logic T. Nipkow and L.C. Paulson and M. Wenzel: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Springer LNCS 2283, 2002.
General Information
- Language
- English
- Levels
- BSC , DS , MSC
- Frequency
- Yearly recurring
Examination
- Type
- session examination
- Mode
- oral 30 minutes
Course Components
| Type | Title | Time & Place | Hours |
|---|---|---|---|
| lecture | Computer-Supported Modeling and Reasoning |
|
2 h weekly |
| exercise | Computer-Supported Modeling and Reasoning |
|
2 h weekly |