703315 VU Logik und Lernen B: Interactive Theorem Proving in Isabelle/HOL

Sommersemester 2023 | Stand: 12.01.2023 | LV auf Merkliste setzen

Institut:

Institut für Informatik

Lektor/in/n/en:

assoz. Prof. Dr. René Thiemann, +43 512 507 53234

LV-Nummer:

703315

Titel:

VU Logik und Lernen B: Interactive Theorem Proving in Isabelle/HOL

Typ/Stunden:

VU 3

ECTS-AP:

Rhythmus:

wöch.

Wiederholungsturnus:

jährlich

Unterrichtssprache:

Englisch

Lernergebnis:

Verständnis von Interaktiven Beweisern; Kenntnisse, Programme in Isabelle/HOL zu spezifizieren und formal zu verifizieren; Erwerb der Fertigkeit, sich selbständig auf dem Gebiet weiterzubilden.

Inhalt:

Dieser Kurs bietet eine Einführung in Interaktives Beweisen mit einem Schwerpunkt auf den Beweis-Assistenten Isabelle und Logik höherer Ordnung (HOL). Die folgenden Themen werden behandelt:

Logik höherer Ordnung
Isabelles Beweis Sprache Isar
Natürliches Schließen in Isabelle
Funktionale Programmierung in Isabelle
Induktive Definitionen
Code-Generierung
Auswahl von weiterführenden Themen

Datenschutzhinweis:

LV wird aufgezeichnet

OLAT:

https://lms.uibk.ac.at/url/RepositoryEntry/5373624454

Link:

http://cl-informatik.uibk.ac.at/teaching/ss23/itpIsa

Beginn:

siehe Termine

Studienzuordnung(en)

Fakultät für Mathematik, Informatik und Physik

Masterstudium Informatik nach dem Curriculum 2021 (120 ECTS-AP, 4 Semester)

Wahlmodule (50 ECTS-AP)

Wahlmodul 7: Logik und Lernen (10 ECTS-AP, 6 SSt.)

Nachhaltigkeitsziele

SDG 4 - Hochwertige Bildung: Inklusive, gleichberechtigte und hochwertige Bildung gewährleisten und Möglichkeiten lebenslangen Lernens für alle fördern
SDG 9 - Industrie, Innovation und Infrastruktur: Eine widerstandsfähige Infrastruktur aufbauen, breitenwirksame und nachhaltige Industrialisierung fördern und Innovationen unterstützen

Termine

Gruppe 0	Termine dieser Gruppe als iCalendar (.ics) exportieren Hilfe
Datum	Uhrzeit	Ort
Do 09.03.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 16.03.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 23.03.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 30.03.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 20.04.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 27.04.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 04.05.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 11.05.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 25.05.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 01.06.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 15.06.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 22.06.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei
Do 29.06.2023	09.15 - 12.00	rr 20 rr 20	Barrierefrei