    Course module   NWIIPI004  Category   PB (Propaedeutic)  Language of instruction   English  Offered by   Radboud University; Faculty of Science; Informatica en Informatiekunde;  Lecturer(s)     Academic year   2018   Period   KW3KW4  (28/01/2019 to 01/09/2019) 
 Starting block   KW3  
 Course mode   fulltime  
 Remarks   Formerly "Beweren en Bewijzen"; as of 2017, taught in English. First access for students for whom course is compulsory  Registration using OSIRIS   Yes  Course open to students from other faculties   Yes  Preregistration   No  Waiting list   No  Placement procedure   In order of Study programme  Explanation   In order of Study programme 
     
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
 take part actively and constructively in making unclear assertions clear
 structurize text using definitions
 indicate the distinctions between natural languages and formal languages
 deal in a professional way with different notations for intrinsically the same language
 Specific competencies with respect to logic:
 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 without reasonable doubt
 Specific competencies with respect to system modelling:
 create a rationality square for a given artifact
 specify important properties of simple realtime systems and their components within predicate logic
 prove correctness of specifications in predicate logic
 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. 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 practised in relatively small weekly obligatory 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.




This course was previously known as 'Beweren en Bewijzen' and 'Assertion and Argumentation'. 
 The rationality square.  The focus of a model.  Natural languages and formal languages.  Propositional logic and predicate logic: syntax and semantics.  Systematic translation of assertions in natural language to assertions in predicate logic.  Proofs in natural language.  Proofs in formal language using truth tables, semantic tableaux and natural deduction.  Using a proof assistant.  Correctness theorem of an artifact. 

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 Coqpracticum: the average score C of the weekly Coq assignments must be at least 5.5.
In addition there are nonmandatory weekly assignments; these assignments are not graded, but act as an entrance ticket for the response lectures: only students who handed in a serious attempt for these learning tasks are admitted to the response lectures. Participation in these response lectures may lead to a small bonus B for the final grade.
Under the assumption that all requirements for the obligatory parts are met, the final grade F is MIN(10, ((IE1+IE2)/2 + P)/2 + B).
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. 

You need to have basic knowledge of proposition and predicate logic on the level of the courses Formal Reasoning (IPK001) or Mathematical Structures (IPC020). In addition, some experience with programming and modeling will be practical. 
   Recommended materialsBookLogic in Computer Science, by Huth and Ryan. This book is useful for background information, but there is no obligation to use this book within the course. 
ISBN  :   9780521543101 
Title  :   Logic in Computer Science 
Author  :   Huth and Ryan 


Instructional modesCourseAttendance Mandatory   Yes 
Remark168 hours.
 Lecture Remark28 hours.
 ProjectAttendance Mandatory   Yes 
GeneralA mandatory part of this course is a large group assignment. Remark20 hours.
 Response lecture GeneralAt the beginning of the course the response lectures are 45 minutes. However, near the end of the course, usually groups are combined to give lectures of 90 minutes. Preparation of meetingsIt is obligatory to hand in the learning task to be admitted to the response lecture. Remark14 hours.
 Self study Remark78 hours.
 Tutorial Remark28 hours.

 TestsIntermediate Test 1Test weight   0 
Test type   Test 
Opportunities   Block KW3, Block KW4 
 Intermediate Test 2Test weight   0 
Test type   Test 
Opportunities   Block KW4, Block KW4 
 ProjectTest weight   0 
Test type   Project 
Opportunities   Block KW4, Block KW4 
 Coq AssignmentsTest weight   0 
Test type   Assignment 
Opportunities   Block KW4, Block KW4 
 Final GradeTest weight   1 
Test type   Exam 
Opportunities   Block KW4, Block KW4 


  
 
 