Theorem Proving with LEAN

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Theorem Proving with LEAN

Lehrveranstaltung mit SWS 0/0/4 (Vorlesung/Übung/Praktikum) in WS 2022


Umfang (SWS)

  • 0/0/4



  • Referat


This course is offered for the "Komplexpraktikum Wissensbasierte Systeme" in WS 2022/23 within the module INF-B-510.

The goal of this course is to give a practical introduction to the LEAN interactive theorem prover. To this aim students are asked to formalize various definitions and results from the undergraduate lecture "Formale Systeme" in the LEAN language. After an introductory session, a weekly option for consultation will be offered. The individual results are presented in a colloquium at the end of the semester.

Additional information and updates will be communicated through the matrix channel.

Veranstaltungskalender abonnieren (icalendar)

Praktikum First Meeting DS4, 26. Oktober 2022 in APB 3027