HS "Reading Club: Deductive Theorem Proving" (SS 07)

Thema

Aufbauend auf den in den Vorlesungen und Übungen des Faches Kognitive Systeme erworbenen Kenntnissen und Fertigkeiten wird im Seminar die eigenständige Erarbeitung und Präsentation eines Themengebiets auf der Basis von wissenschaftlicher Literatur eingeübt. Dabei werden Kompetenzen zur Einarbeitung in vertiefende Fragestellungen anhand wissenschaftlicher Literatur sowie deren Präsentation in mündlicher und schriftlicher Form erworben.

Lernziele
Im Seminar werden vertiefende Aspekte aus dem Bereich Maschinelles Lernen oder Automatisches Programmieren anhand einer speziellen Schwerpunktsetzung durch Seminarvorträge und schriftliche Ausarbeitung vertiefend erarbeitet. Thema

Based on the knowledge and skills gained in the lectures and exercises in the domain of cognitive systems, in this seminar course we are concerned with the reception and presentation of scientific papers concerning a specific research topic. You will acquire skills for obtaining up-to-date knowledge in some specific domain by reading scientific texts and in their oral and written presentation.

Objectives
In this seminar course we will get acquainted with specific aspects from the domain of machine learning or automated programming by seminar talks and written reports. Topic
Automated Deductive Reasoning with ISABELLE.
Joint Course with Theoretical Computer Science.
Webpage with current information
Current Topic (SS 07)
Participants should have a good understanding of basic predicate logic (FOL and Fitch Calculus) and have some experience (or at least strong interest!) in functional programming (e.g., ML, Haskell, Lisp). Prerequisites

Anrechenbarkeit und Leistungsnachweise

Informationen auf der Seite Lehre der Gruppe CogSys im Überblick.

Topics and Presenters

A Simple Theory of Types (Church/Paulson), Peter Wullinger. [pdf]

vorauss. 16.5.2007 statt 9.5.2007

Functional Programming in HOL, Martin Hofmann. [pdf]

23.5.2007

More Functional Programming, Dominik Mayer. [pdf]

30.5.2007

The Rules of the Game, Joaquin Aguado. [pdf]

13.6.2007

The Rules of the Game II, Stephan Scheele. [pdf]

27.6.2007

Sets, Functions and Relations, Emanuel Kitzelmann.

18.7.07, 10 Uhr, s.t.

Grundlagenliteratur und Links

  • T. Nipkow, L. C. Pauslon, M. Wenzel: Isabelle/Hol: A Proof Assistant for Higher-order Logic. Springer 2002
  • Alonzo Church, "A Formulation of the Simple Theory of Types," Journal of Symbolic Logic, Vol. 5, 1940, 56-68.
  • Lawrence C. Paulson, A Formulation of the Simple Theory of Types (for Isabelle), 1989.
Literature