Moses - Einführung in das interaktive Theorembeweisen

Zur Modulseite PDF generieren

Modul / Version
#40416 / #1

Gültigkeit
WS 2013/14 - WS 2015/16

Verfügbare Sprache(n)
Deutsch

Titel des Moduls
Einführung in das interaktive Theorembeweisen

Leistungspunkte
3

Modulverantwortliche*r
Nestmann, Uwe

Benotung
Benotet

Prüfungsform
Mündliche Prüfung

Lehrsprache(n)
Deutsch

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
EN 24

Ansprechpartner*in
Karsten, Nadine

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

Webseite

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

Diese Modulbeschreibung gilt nicht im aktuellen Semester.

Die Modulbeschreibung gilt nur für den Zeitraum WS 2013/14 - WS 2015/16. Die Version für das aktuelle Semester (SoSe 2025) finden Sie hier: Modulbeschreibung des SoSe 2025

Lernergebnisse

Werkzeug-Kompetenz im Umgang mit dem Theorembeweiser Isabelle. Grundverständnis bei der Erstellung mechanisch formalisierbarer Beweise. Kompetenz bei der konkreten Umsetzung von informallen Beweisideen in Isabelle-Code. Das Modul vermittelt überwiegend: Fachkompetenz 30x Methodenkompetenz 30x Systemkompetenz 30x Sozialkompetenz 10x

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:

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

ISIS-Kurssuche nach Veranstaltungen des Moduls

Arbeitsaufwand und Leistungspunkte

Einführung in das interaktive Theorembeweisen (IV):

Aufwandbeschreibung	Multiplikator	Stunden	Gesamt
Präsenzzeit	15.0	2.0h	30.0h
Vor-/Nachbearbeitung	15.0	4.0h	60.0h
			90.0h(~3 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 Übung mit Isabelle, eventuell mit Vortrag über Fallstudien. Im September 2014 geplant für die zweite/dritte Woche.

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

Dauer/Umfang

Keine Angabe

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 ISIS-Kurs. Vorab-Informationen dazu rechtzeitig über http://www.mtv.tu-berlin.de/menue/lehre/

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.

Studierende anderer Studiengänge können dieses Modul ohne Kapazitätsprüfung belegen.

Informatik - Diplom (Studiengebiet THI) Technische Informatik - Diplom

Sonstiges

Keine Angabe