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.)122SoSe 2020SoSe 2025
Computer Science (Informatik) (M. Sc.)144SoSe 2020SoSe 2025
Elektrotechnik (M. Sc.)122SoSe 2020SoSe 2025
Informatik (B. Sc.)111SoSe 2020SoSe 2025
Information Systems Management (Wirtschaftsinformatik) (M. Sc.)114SoSe 2020SoSe 2025
Wirtschaftsingenieurwesen (M. Sc.)112SoSe 2020SoSe 2025

Sonstiges

Keine Angabe