Moses - Introduction into Interactive Theorem Proving

Display language

To modulepage Generate PDF

Module / Version:
#40416 / #4

Validity:
Seit SoSe 2020

Default display language:
English

Module title:
Introduction into Interactive Theorem Proving

Credits:
3

Responsible person:
Nestmann, Uwe

Grading:
benotet

Type of exam:
Mündliche Prüfung

Zugehörigkeit

Faculty:
Fakultät IV

Institute:
Institut für Softwaretechnik und Theoretische Informatik

Area of expertise:
34351900 FG Modelle und Theorie Verteilter Systeme (MTV)

Prüfungsausschuss:
No information

Kontakt

Office:
TEL 7-2

Contact person:
Karsten, Nadine

E-mail address:
lehre@mtv.tu-berlin.de

Website:

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

Learning Outcomes

Competencies in the usage of the Interactive Theorem-Proving Environment Isabelle/HOL. Solid understanding on the production of mechanically checkable proofs. Competencies in the transformation of informal proof ideas into Isabelle code.

Content

Higher-order logic (HOL); Isabelle syntax; Proof strategies; Induction and co-induction; Representation of theories in Isabelle/HOL; Difference between „deep“ versus „shallow“ embeddings.

Module Components

Pflichtteil:

All Courses are mandatory.

Course Name	Type	Number	Cycle	Language	SWS	VZ
Einführung in das interaktive Theorembeweisen	IV	0434 L 362	SoSe	No information	2

Workload and Credit Points

Einführung in das interaktive Theorembeweisen (IV):

Workload description	Multiplier	Hours	Total
Individual study (preparation and consolidation)	5.0	3.0h	15.0h
Presence	5.0	6.0h	30.0h
			45.0h(~2 LP)

Course-independent workload:

Workload description	Multiplier	Hours	Total
Exam preparation	1.0	45.0h	45.0h
			45.0h(~2 LP)

The Workload of the module sums up to 90.0 Hours. Therefore the module contains 3 Credits.

Description of Teaching and Learning Methods

Block seminar during lecture free-time - 5 days with lectures (introduction to Theorem Proving and Isabelle), practical exercises with Isabelle, depending on the participants: with lectures on case studies.

Requirements for participation and examination

Desirable prerequisites for participation in the courses:

Basic knowledge in formal logic; knowledge and competences in proving.

Mandatory requirements for the module test application:

This module has no requirements.

Module completion

Grading

graded

Type of exam

Oral exam

Language

German/English

Duration/Extent

30-40 min

Duration of the Module

The following number of semesters is estimated for taking and completing the module:
1 Semester.

This module may be commenced in the following semesters:
Sommersemester.

Maximum Number of Participants

The maximum capacity of students is 20.

Registration Procedures

If you are interested, please sign in to the current course on ISIS. The registration for the module examination takes place at the examination office or via the QISPOS platform. POS examination number: 60836

Recommended literature
Material erhältlich über http://isabelle.in.tum.de/

Assigned Degree Programs

Semester:

Zeige auch ausgelaufene Studiengänge und StuPOs

This module is used in the following Degree Programs (new System):

Studiengang / StuPO	StuPOs	Verwendungen	Erste Verwendung	Letzte Verwendung
Computer Engineering (M. Sc.)	1	18	SoSe 2020	SoSe 2024
Computer Science (Informatik) (M. Sc.)	1	36	SoSe 2020	SoSe 2024
Elektrotechnik (M. Sc.)	1	18	SoSe 2020	SoSe 2024
Informatik (B. Sc.)	1	9	SoSe 2020	SoSe 2024
Information Systems Management (Wirtschaftsinformatik) (M. Sc.)	2	12	SoSe 2020	SoSe 2024
Wirtschaftsingenieurwesen (M. Sc.)	1	10	SoSe 2020	SoSe 2024

Miscellaneous

No information

Introduction into Interactive Theorem Proving