    Cursus   NWIIPI004  Categorie   BA (Bachelor)  Voertaal   Engels  Aangeboden door   Radboud Universiteit; Faculteit der Natuurwetenschappen, Wiskunde en Informatica; Informatica en Informatiekunde;  Docenten     Collegejaar   2022   Periode   KW3KW4  (30012023 t/m 31082023) 
 Aanvangsblok   KW3  
 Onderwijsvorm   voltijd  
 Opmerking   Studenten voor wie de cursus verplicht is hebben voorrang.  Inschrijven via OSIRIS   Ja  Inschrijven voor bijvakkers   Ja  Voorinschrijving   Nee  Wachtlijst   Nee  Plaatsingsprocedure   Volgorde bepaald door opl./programma  Toelichting   Volgorde bepaald door opleiding/programma 
     
After completing this course participants are able to:
 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
 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
 Specific competencies with respect to system modeling:
 create a rationality square for a given artifact
 specify important properties of simple realtime 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



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. The 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, in particular using natural deduction. Eventually, you will use a proof assistant to check your proof.
In addition to the theory behind this main topic of specifying how systems (should) work and formally proving that they indeed act according to their specifications, the course also provides an introduction to the following topics: structural induction, modal logic, Kripke semantics, and natural deduction for modal logic.
These techniques will be practiced in relatively small weekly exercises. They will be tested in written intermediate digital exams and in a group project where you will show that you can apply these techniques of assertion and argumentation on a complex system.
Instructional Modes
The weekly learning cycle starts with a two hour plenary lecture. After that, students have to work in groups of two on a weekly task. During a two hour plenary tutorial they can ask questions about this task. The learning cycle ends with a group tutorial where students can get feedback on their solutions.
In addition, students have to work in groups of four on a large group project.


 
You need to have basic knowledge of propositional and predicate logic on the level of the courses IPK001 Introduction to Formal Reasoning or IPC020 Mathematical Structures. It helps if you already did the course IPC002 Languages and Automata or some other course where you have seen context free grammars.


The obligatory parts of this course are:
 Two interim exams which give the scores IE1 and IE2;
 the score on both IE1 and IE2 must be at least 4.0,
 and 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 Coqpracticum (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 + P)/3+C/10). In all other situations, the final grade F is MIN(5, (IE1 + IE2 + P)/3). Final grades will be rounded in the normal way.


This is a course for which it is essential that you practice a lot. And that is exactly the role of the Coq practicum (also known as the weekly assignments). Therefore, doing an interim exam is directly coupled to doing the corresponding part of the Coq practicum in the same edition of the course. So even if you passed the Coq practicum in a previous year, but have to (re)do, for instance, the second interim exam, then you will have to pass the second part of the Coq practicum this year again, so you are enforced to practice in time.
Grades for the project and the interim exams can be reused, as long as they comply to the current minimum requirements.




   Verplicht materiaalHandoutsHandouts of the slides will be published in Brightspace. 


Aanbevolen materiaalBoekThis 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 


WerkvormenCourseAanwezigheidsplicht   Ja 
Opmerking168 hours.

 ToetsenDigital Intermediate Test 1Weging   0 
Toetsvorm   Digitale toets met CIRRUS 
Gelegenheden   Blok KW3, Blok KW4 
 Digital Intermediate Test 2Weging   0 
Toetsvorm   Digitale toets met CIRRUS 
Gelegenheden   Blok KW4, Blok KW4 
 ProjectWeging   0 
Toetsvorm   Project 
Gelegenheden   Blok KW4, Blok KW4 
 Coq AssignmentsWeging   0 
Toetsvorm   Opdracht 
Gelegenheden   Blok KW4, Blok KW4 
 Final GradeWeging   1 
Toetsvorm   Tentamen 
Gelegenheden   Blok KW4, Blok KW4 


  
 
 