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:Seminar Room GÖDEL (link still missing)
Favoritenstraße 9 / ground floor (entry from court yard)
Registration: via TUWIS++, or if this fails, by email to chrisf@logic.at.
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.
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.
C.Fermüller