Logic and Modelling

2018-2019
Dit vak wordt in het Engels aangeboden. Omschrijvingen kunnen daardoor mogelijk alleen in het Engels worden weergegeven.

Doel vak

The course objective is to obtain a good knowledge and understanding of
the most important logical systems: propositional logic, predicate logic
and modal logic. The students learn to use these systems to model data,
knowledge and actions. An important aspect of the course is the ability
to reason using these logics and reason about these logics: what can and
what can not be expressed with a logic system, and what are the
differences between the systems with respect to expressive power or the
existence of decision procedures.

Inhoud vak

The focus of the lecture is on propositional logic and first-order
predicate logic. We work with natural deduction as proof system. The
relation between semantic and syntactic methods is important; the
central keywords are correctness, consistency and completeness.
Moreover, we pay attention to expressive power, for example when
formulating queries. A fundamental tool, for this purpose, is the
compactness theorem.

Algorithmically there the contrast between the decidability of
propositional logic and the undecidability of predicate logic (for
example, seen by a coding of the Post Correspondence Problem).

As a variation of the mentioned logics, we consider modal logic with
Kripke models as semantics.

Onderwijsvorm

Lecture, exercise classes and computer practicum using the Lean proof
assistant.

Toetsvorm

Exam and computer assignments using the Lean proof assistant.

Literatuur

Mandatory:

Jeremy Avigad, Robert Y. Lewis, Floris van Doorn, Logic and Proof
https://leanprover.github.io/logic_and_proof/

Recommended:

Michael Huth, Mark Ryan, Logic in Computer Science (2nd edition)
Cambridge University Press, 2004 ISBN 0 521 54310 X

Doelgroep

2CS

Aanbevolen voorkennis

Logic and Sets

Algemene informatie

Vakcode X_401015
Studiepunten 6 EC
Periode P5
Vakniveau 200
Onderwijstaal Engels
Faculteit Faculteit der Bètawetenschappen
Vakcoördinator dr. R.Y. Lewis
Examinator dr. R.Y. Lewis
Docenten dr. J.C. Blanchette
dr. R.Y. Lewis

Praktische informatie

Voor dit vak moet je zelf intekenen.

Voor dit vak kun je last-minute intekenen.

Werkvormen Werkcollege, Deeltoets extra zaalcapaciteit, Hoorcollege, Practicum
Doelgroepen

Dit vak is ook toegankelijk als: