Moses - Introduction into Interactive Theorem Proving

Anzeigesprache

Diese Modulbeschreibung gilt nicht im aktuellen Semester.

Die Modulbeschreibung gilt nur für den Zeitraum SS 2017 - WS 2019/20. Die Version für das aktuelle Semester (SoSe 2024) finden Sie hier: Modulbeschreibung des SoSe 2024

Modul / Version:
#40416 / #3

Gültigkeit:
SS 2017 - WS 2019/20

Standard-Anzeigesprache:
Deutsch/Englisch

Titel des Moduls:
Introduction into Interactive Theorem Proving
Einführung in das interaktive Theorembeweisen

Leistungspunkte:
3

Modulverantwortliche*r:
Nestmann, Uwe

Benotung:
benotet

Prüfungsform:
Mündliche Prüfung

Zugehörigkeit

Fakultät:
Fakultät IV

Institut:
Institut für Softwaretechnik und Theoretische Informatik

Fachgebiet:
34351900 FG Modelle und Theorie Verteilter Systeme (MTV)

Prüfungsausschuss:
Keine Angabe

Kontakt

Sekretariat:
TEL 7-2

Ansprechpartner*in:
Karsten, Nadine

E-Mail-Adresse:
lehre@mtv.tu-berlin.de

Webseite:

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

Pflichtteil:

Die folgenden Veranstaltungen sind für das Modul obligatorisch:

Lehrveranstaltungen	Art	Nummer	Turnus	Sprache	SWS	VZ
Einführung in das interaktive Theorembeweisen	IV	0434 L 362	SoSe	Keine Angabe	2

Arbeitsaufwand und Leistungspunkte

Einführung in das interaktive Theorembeweisen (IV):

Aufwandbeschreibung	Multiplikator	Stunden	Gesamt
Präsenzzeit	5.0	6.0h	30.0h
Vor-/Nachbearbeitung	5.0	3.0h	15.0h
			45.0h(~2 LP)

Lehrveranstaltungsunabhängiger Aufwand:

Aufwandbeschreibung	Multiplikator	Stunden	Gesamt
Prüfungsvorbereitung	1.0	45.0h	45.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

Sprache

Deutsch/Englisch

Dauer/Umfang

30-40 Minuten

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.

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

Semester:

Zeige auch ausgelaufene Studiengänge und StuPOs

Diese Modulversion wird in folgenden Studiengängen verwendet:

	Studiengang / StuPO	StuPOs	Verwendungen	Erste Verwendung	Letzte Verwendung
Dieses Modul findet in keinem Studiengang Verwendung.

Sonstiges

Keine Angabe