1. Modulverzeichnis (MTS)
  2. Module
  3. Modulbeschreibung anzeigen

Einführung in das interaktive Theorembeweisen

Zur Modulseite PDF generieren

#40416 / #4

Seit SoSe 2020

Deutsch

Introduction into Interactive Theorem Proving
Einführung in das interaktive Theorembeweisen

3

Nestmann, Uwe

Benotet

Mündliche Prüfung

Englisch

Zugehörigkeit


Fakultät IV

Institut für Softwaretechnik und Theoretische Informatik

34351900 FG Modelle und Theorie Verteilter Systeme (MTV)

Keine Angabe

Kontakt


EN 24

Karsten, Nadine

lehre@mtv.tu-berlin.de

http://www.mtv.tu-berlin.de/menue/lehre/module/isabellelab/

Lernergebnisse

Werkzeug-Kompetenz im Umgang mit dem Theorembeweiser Isabelle/HOL. Grundverständnis bei der Erstellung mechanisch formalisierbarer Beweise. Kompetenz bei der konkreten Umsetzung von informallen Beweisideen in Isabelle-Code.

Lehrinhalte

Higher-Order Logik (HOL); Isabelle-Syntax; Beweisstrategien; Induktion und Co-Induktion; Darstellungen von Theorien in Isabelle/HOL; Unterschied von „deep“ versus „shallow“ Einbettungen.

Modulbestandteile

Pflichtbereich

Die folgenden Veranstaltungen sind für das Modul obligatorisch:

LehrveranstaltungenArtNummerTurnusSpracheSWS ISIS VVZ
Einführung in das interaktive TheorembeweisenIV0434 L 362SoSeKeine Angabe2
ISIS-Kurssuche nach Veranstaltungen des Moduls

Arbeitsaufwand und Leistungspunkte

Einführung in das interaktive Theorembeweisen (IV):

AufwandbeschreibungMultiplikatorStundenGesamt
Präsenzzeit5.06.0h30.0h
Vor-/Nachbearbeitung5.03.0h15.0h
45.0h(~2 LP)

Lehrveranstaltungsunabhängiger Aufwand:

AufwandbeschreibungMultiplikatorStundenGesamt
Prüfungsvorbereitung1.045.0h45.0h
45.0h(~2 LP)
Der Aufwand des Moduls summiert sich zu 90.0 Stunden. Damit umfasst das Modul 3 Leistungspunkte.

Beschreibung der Lehr- und Lernformen

Blockveranstaltung in der vorlesungsfreien Zeit — 5 Tage mit VL (Einführung in Theorem Beweiser und Isabelle), praktische Übungen mit Isabelle, je nach Teilnehmern mit Vorträgen über Fallstudien.

Voraussetzungen für die Teilnahme / Prüfung

Wünschenswerte Voraussetzungen für die Teilnahme an den Lehrveranstaltungen:

Grundkenntnisse in Formaler Logik; Kenntnisse und Kompetenzen im Führen von Beweisen.

Verpflichtende Voraussetzungen für die Modulprüfungsanmeldung:

Dieses Modul hat keine Prüfungsvoraussetzungen.

Abschluss des Moduls

Benotung

Benotet

Prüfungsform

Mündliche Prüfung

Sprache(n)

Deutsch, Englisch

Dauer/Umfang

30-40 Minuten

Prüfungsbeschreibung (Abschluss des Moduls)

Mündliche Prüfung Zulassungsbedingung: aktive Mitarbeit durch Lösen praktischer Übungen und Vorträge

Dauer des Moduls

Für Belegung und Abschluss des Moduls ist folgende Semesteranzahl veranschlagt:
1 Semester.

Dieses Modul kann in folgenden Semestern begonnen werden:
Sommersemester.

Maximale teilnehmende Personen

Die maximale Teilnehmerzahl beträgt 20.

Anmeldeformalitäten

Interessensbekundung durch Anmeldung im jeweiligen ISIS-Kurs. Die Anmeldung zur Modulprüfung erfolgt im Prüfungsamt bzw. über QISPOS. POS-Prüfungsnummer: 60836

Literaturhinweise, Skripte

Skript in Papierform

Verfügbarkeit:  nicht verfügbar

 

Skript in elektronischer Form

Verfügbarkeit:  nicht verfügbar

 

Literatur

Empfohlene Literatur
Material erhältlich über http://isabelle.in.tum.de/

Zugeordnete Studiengänge


Diese Modulversion wird in folgenden Studiengängen verwendet:

Studiengang / StuPOStuPOsVerwendungenErste VerwendungLetzte Verwendung
Computer Engineering (M. Sc.)124SoSe 2020WiSe 2025/26
Computer Science (Informatik) (M. Sc.)148SoSe 2020WiSe 2025/26
Elektrotechnik (M. Sc.)124SoSe 2020WiSe 2025/26
Informatik (B. Sc.)112SoSe 2020WiSe 2025/26
Information Systems Management (Wirtschaftsinformatik) (M. Sc.)115SoSe 2020WiSe 2025/26
Wirtschaftsingenieurwesen (M. Sc.)113SoSe 2020WiSe 2025/26

Sonstiges

Keine Angabe