[ Lehrveranstaltungen 185/2 ]     [ AG Theoretische Informatik und Logik ]     [ Fachbereich Informatik ]     [ Technische Universität Wien ]

3.0/2.0 VU Higher-order Logic (185.301)

Lehrveranstaltungsleiter: Christian Fermüller

Diese Lehrveranstaltung ist ein Wahlfach in den Magisterstudien Computational Intelligence und Intelligente Systeme.

This course also belongs to the foundation module Advanced Logic of the international Master Programme in Computational Logic.

This course will be held in English.

Contents of this page:
  • Topic - contents of the course
  • Prerequisites
  • Meetings
  • Handouts
  • Hints for submitting exercises
  • Evaluation/credits
  • Further links

  • *** Recent information (SS 2011) ***

    Topic - contents of the course

    Basic Principles of Higher-order Logic

    Higher-order logic differs from first-order logic in admitting several types of variables for quantification: besides individual variables we may quantify over predicate variables, function variables etc. This extension substantially increases the expressive power of the logic. We obtain an elegant framework for the specification of mathematical concepts and theories, in particular also induction principles and cardinality constraints. We will explore fundamental differences between first order and higher order logics and stress the use of logic as a specification language. The focus is on second order logics, but also higher types and logics between first and second order will be explored.


    This is an advanced course in logic.
    Firm knowledge of classical first-order logic is a prerequite.

    TEST YOURSELF whether you are fit for this course:
    You should be able to provide precise definitions and explanations of the following basic concepts: free and bound variables in first order formulas (fofs), model/interpretation of fofs, constants vs. domain elements, truth vs. validity, satisfiability, logical consequence vs. derivability, soundness and completeness of a given proof system.
    You also should have no troubles to write down an fof that is only satisfiable in infinite domains as well as an fof (involving identity) that expresses that there are exactly 3 domain elements.


    Various course material - in particular copies of the lecture slides - will be made available here (and/or in the lecture) to all participants.

    Hints for the submission of exercises

    HINT: For the presentation of formal derivations in LaTeX we recommend bussproofs.sty.
    This and other useful style files are available from Latex for Logicians).

    Include the problem statement, its number (`Exercise X: ... ') and your name in the submitted solution files. Send corresponding (uncompressed) PDF files to Chris Fermüller.


    The evaluation will mainly be based on the amount and quality of submitted solutions to the exercises (as assigned during the course).
    In special cases, the alternative of a (written + oral) examination will be offered.

    Further links

    Will be expanded during the semester.
    Valid HTML 4.01! Viewable With Any Browser C.Fermüller