NWI-IPI004
Logic and Applications
Cursus informatieRooster
CursusNWI-IPI004
Studiepunten (ECTS)6
CategorieBA (Bachelor)
VoertaalEngels
Aangeboden doorRadboud Universiteit; Faculteit der Natuurwetenschappen, Wiskunde en Informatica; Informatica en Informatiekunde;
Docenten
Coördinator		dr. E.G.M. Hubbers
Overige cursussen docent
Examinator		dr. E.G.M. Hubbers
Overige cursussen docent
Contactpersoon van de cursus		dr. E.G.M. Hubbers
Overige cursussen docent
Docent		dr. E.G.M. Hubbers
Overige cursussen docent
Docent		N.M. van der Weide
Overige cursussen docent
Collegejaar2019
Periode
KW3-KW4  (03-02-2020 t/m 30-08-2020)
Aanvangsblok
KW3
Onderwijsvorm
voltijd
OpmerkingStudenten voor wie de cursus verplicht is hebben voorrang.
Inschrijven via OSIRISJa
Inschrijven voor bijvakkersJa
VoorinschrijvingNee
WachtlijstNee
PlaatsingsprocedureVolgorde bepaald door opl./programma
ToelichtingVolgorde bepaald door opleiding/programma
Cursusdoelen
After completing this course participants are able to:
  1. General competencies:
    • detect inconsistencies and mistakes in wrongly formulated statements
    • formulate clear, consistent and correct assertions
    • provide argumentation about the correctness of your own assertions
    • systematically derive solutions
    • make unclear assertions clear
    • structurize text using definitions
    • create simple proofs by structural induction
  2. Specific competencies with respect to logic:
    • deal in a professional way with different notations for intrinsically the same language
    • recognize which problems can be solved and which problems cannot be solved using propositional logic
    • translate natural language assertions into logic in a systematic way
    • present the semantics of formulas in propositional or predicate logic in a clear way in natural language
    • explain the semantics of the rules for natural deduction
    • prove assertions using natural deduction
    • present proofs in a comprehensible way
    • derive truth tables for assertions in propositional logic
    • derive semantic tableaux for assertions in propositional logic
    • use the terminology of tautology, logical consequences, and logical equivalences
    • recognize and indicate mistakes within proofs
    • use the proof assistant Coq to prove theorems
    • derive the Kripke semantics of formulas in modal logic
  3. Specific competencies with respect to system modeling:
    • create a rationality square for a given artifact
    • specify important properties of simple real-time systems and their components within predicate logic
    • prove the correctness of specifications in propositional logic or predicate logic using an appropriate method
    • divide systems hierarchically into their components
    • prove that a system complies to certain properties using specifications in predicate logic of its components
    • clearly present an analysis, a design and a correctness proof of a system
Inhoud
This is a course in applied logic. On the one hand, you will learn how to specify systems both informally in natural language and formally using propositional or predicate logic. Our goal is to describe these systems in such a way that these specifications can be used as a contract. On the other hand, you will learn how to prove these assertions, or in other words, to prove that these systems operate exactly as they should according to their contracts. This process of argumentation will also be done using natural language and using formal mathematical methods. Eventually, you will use a proof assistant to check your proof.
These techniques will be practiced in relatively small weekly exercises. They will be tested in written intermediate exams and a group project in which you will show that you can apply these techniques of assertion and argumentation on a complex system.
In addition, a short introduction is given about structural induction and about Kripke semantics in modal logic.
Niveau

Voorkennis
You need to have basic knowledge of propositional and predicate logic on the level of the courses Formal Reasoning or Mathematical Structures. It helps if you already did the course Languages and Automata.
Toetsinformatie
The obligatory parts of this course are: - Two interim exams which give the scores IE1 and IE2; the average score of IE1 and IE2 must be at least 5.0. - A group project; the score P for this project must be at least 5.5. - A Coq-practicum (also known as weekly tasks): the average score C of these weekly tasks must be at least 5.5. Under the assumption that all requirements for the obligatory parts are met, the final grade F is MIN(10, ((IE1+IE2)/2 + P)/2). In all other situations, the final grade F is MIN(5, ((IE1+IE2)/2 + P)/2). Final grades will be rounded in the normal way.
Bijzonderheden
This course was previously known as 'Beweren en Bewijzen' and 'Assertion and Argumentation'.
Bijzonderheden
This course was previously known as 'Beweren en Bewijzen' and 'Assertion and Argumentation'.

Onderwerpen
- System development (artifacts, rationality squares, foci, domain models, functional networks, components, specifications, correctness theorems)
- Grammar (propositional logic, predicate logic)
- Systematic translation (natural language to predicate logic)
- Proof rules (natural language, natural deduction)
- Proofs (natural language, truth tables, semantic tableaux in propositional logic, natural deduction in propositional logic and predicate logic, structural induction)
- Using the proof assistant Coq
- Modal logic (Kripke models, S5)

Toetsinformatie
The obligatory parts of this course are:
- Two interim exams which give the scores IE1 and IE2; the average score of IE1 and IE2 must be at least 5.0.
- A group project; the score P for this project must be at least 5.5.
- A Coq-practicum (also known as weekly tasks): the average score C of these weekly tasks must be at least 5.5.

Under the assumption that all requirements for the obligatory parts are met, the final grade F is MIN(10, ((IE1+IE2)/2 + P)/2).

In all other situations, the final grade F is MIN(5, ((IE1+IE2)/2 + P)/2).

Final grades will be rounded in the normal way.

Voorkennis
You need to have basic knowledge of propositional and predicate logic on the level of the courses Formal Reasoning or Mathematical Structures. It helps if you already did the course Languages and Automata.

Aanbevolen materiaal
Boek
This book is useful for background information, but we don't actively use it within the course.
ISBN:9780521543101
Titel:Logic in Computer Science
Auteur:Huth and Ryan
Uitgever:Cambridge University Press

Werkvormen
Course
AanwezigheidsplichtJa

Opmerking
168 hours.

Lecture

Opmerking
28 hours.

Project
AanwezigheidsplichtJa

Algemeen
Voor dit vak dient er een groepswerkstuk te worden gemaakt.

Opmerking
20 hours.

Response lecture

Algemeen
In het begin van de cursus zijn er groepen van 45 minuten. Aan het eind van de cursus worden er meestal groepen samengevoegd zodat er bijeenkomsten van 90 minuten ontstaan.

Voorbereiding bijeenkomsten
Het is verplicht om een leertaak te hebben ingeleverd om deel te mogen nemen aan het responsiecollege.

Opmerking
14 hours.

Self study

Opmerking
78 hours.

Tutorial

Opmerking
28 hours.

Toetsen
Digital Intermediate Test 1
Weging0
ToetsvormDigitale toets met CIRRUS
GelegenhedenBlok KW4, Blok KW4

Digital Intermediate Test 2
Weging0
ToetsvormDigitale toets met CIRRUS
GelegenhedenBlok KW4, Blok KW4

Project
Weging0
ToetsvormProject
GelegenhedenBlok KW4, Blok KW4

Coq Assignments
Weging0
ToetsvormOpdracht
GelegenhedenBlok KW4, Blok KW4

Final Grade
Weging1
ToetsvormTentamen
GelegenhedenBlok KW4, Blok KW4