Computational Logic (21422)

Degree/study: Bachelor's degree in Computer Sciences
Year: 2nd
Term: 3rd
Number of ECTS credits: 4 credits
Hours of study dedication: 100 hours
Teaching language or languages: Catalan, Spanish, English
Teaching Staff: Rafael Ramirez, Victor Dalmau

 

1. Presentation of the subject

The subject Computational Logic is a compulsory subject offered during the bachelor's degree in Computer Science and it is a part of the second year of this degree. The course covers algorithmic and deductive aspects from both propositional and predicate logic, the use of logic to specify, verify and reason about computer programs, and to represent computational problems. The course has two components: one theoretical and one practical. Within the theoretical component, the emphasis is on understanding the concepts at an intuitive level and on the use of mathematical language. 

The course consists of three main activities: lectures, seminars and laboratories. In the lectures, the formal concepts and examples of its applications are introduced. In the seminars, students solve small problems. Each problem corresponds to one of the concepts introduced during the lectures. More computational and complex problems are introduced in laboratories because students have the chance to put the concepts learnt into practice.

 

2. Previous requirements to follow the formative itinerary

The previous knowledge required to follow the course consists of some basic mathematical notions acquired in compulsory secondary education and during the first year of the degree. Specially, the previous knowledge required in the course is: 

- Basic algebraic notions: functions, sets and elementary operations about sets, equivalence relations.
- Basic mathematical logic notions: relations, logical connectors.
- Basic arithmetics.
- Capacity to understand and write basic mathematical expressions in an elemental level.

 

3. Competences to be obtained in the subject

The main objective of this course is that the students acquire the fundamental aspects related to the deductive and algorithmic aspects of propositional and predicate logic and its application to specify, verify and reason about computer programs.

General competences	Specific competences
Instrumental 1. Capacity to reason in an abstract level 2. Cognitive abilities 3. Common sense  Interpersonal 4. Communication skills  Systemic 5. Capacity to identify the best methodology to solve a problem. 6. Capacity to solve problems by combining in a new and not trivial way some known elements 7. Capacity to generate ideas	1. Capacity to understand in an intuitive and formal level the different aspects of propositional and predicate logic: syntax, semantics and its application to different problems of computer science.  2. Capacity to apply the acquired knowledge in practical contexts.  3. Capacity to specify, verify and reason about computer programs and represent computational problems using methods in logic.

 

4. Learning aims

The aim of this course is to extend deductive and algorithmic aspects of propositional and predicate logic, and put into practice its use in order to specify, verify and reason about computer programs, and to represent computational problems. At the same time, students should develop skills to understand the differences between different types of logic and identify the best formalism to specify different computational problems.

 

5.  Evaluation

5.1. General evaluation criteria 

The continuous evaluation takes into account each of the three activities that constitute the course: lectures, laboratories and seminars:
T: theory evaluation through a final exam
L: laboratory evaluation through the programming practical activities and a final exam of practical activities.
S: evaluation of the seminars

In the continuous evaluation, each of the three activities must be passed separately and the final mark is obtained by the weighted average as follows:
Final Mark = 0,6 * T + 0,3 * L + 0,1 * S 

The theory exam will be focused on the contents studied in the theory sessions and in the seminars. It is an individual written exam that evaluates all the skills developed throughout the course. This evaluation is mandatory and it must be qualified with at least 50% to pass the subject. 

A series of practical activities will be taken during the laboratory sessions to test the students' ability to apply theory to write programs on a computer. The practical activities are done in pairs, so that students must learn to communicate and cooperate to solve problems. This evaluation is also mandatory and it must be qualified with at least 50% in order to pass the subject.

Before each seminar session, some problems will be introduced to students to solve them in teams of three before the session, as a previous preparation to the seminar. These problems are related to concepts and knowledge discussed in lectures. Students will be asked to present their solutions to the rest of the class. The evaluation will consider the preparation of the seminar, and the presentation of the solution. The evaluation of the work of the seminars is compulsory and, as stated, the mark S obtained must be qualified with at least 50% to pass the subject.

If the students do not pass the subject with the continuous evaluation explained in the previous points, they have the right of an examination sitting in September. The mark of this sitting will be obtained from an examination of the contents of the lectures and from the mark L. If the student did not pass L in continuous evaluation, he/she will be able to hand in the whole practical activity of the course and it will be evaluated again. Once T and L are passed separately, the mark of September is obtained as follows: 

September mark= 0,6*T+0,4*L  

5.2.  Concretion of competences 

Competences to be obtained in the subject	Achievement indicator	Evaluation procedure	Timing
General competences 1. Capacity to reason in an abstract level 2. Cognitive abilities 3. Common sense 4. Communication skills 5. Capacity to identify the best methodology to solve a problem. 6. Capacity to solve problems by combining in a new and not trivial way some known elements 7. Capacity to generate ideas  Specific competences 1. Capacity to understand in an intuitive and formal level the different aspects of propositional and predicate logic. 2. Capacity to understand algorithmic aspects of the logic like the specification language and the programming of computational problems, and apply this knowledge in the resolution of computational problems in practical contexts. 3. Capacity to put into practice the use of predicate logic to specify, verify and reason about computer programs.	1. Capacity to solve abstract problems 2. Capacity to propose solutions to problems 3. Capacity to propose solutions to problems 4. Coherent well written solutions in practical sessions and seminars 5. Coherent solutions in practical sessions and seminars 6. Coherent solutions in practical sessions and seminars 7. Clever solutions to the problems exposed  1. Capacity to understand mathematical expressions related to propositional and predicate logic syntax and semantics and to specify properties using logic formulas. 2. Capacity to understand and elaborate logic programs to solve practical computational problems. 3. Capacity to specify and verify formally properties of the computer programs and to determine its correctness.	1. Evaluation of practical activities, seminars and the final exam 2. Evaluation of practical activities, seminars and the final exam 3. Evaluation of practical activities, seminars and the final exam 4. Evaluation of practical activities and seminars 5. Evaluation of practical activities and seminars 6. Evaluation of practical activities, seminars and the final exam 7. Evaluation of practical activities, seminars and the final exam  1. Evaluation of seminars and final exam 2. Evaluation of practical activities, seminars and the final exam 3. Evaluation of seminars and final exam	1. During the entire term 2. During the entire term 3. During the entire term 4. During the entire term 5. During the entire term 6. During the entire term 7. During the entire term       1. During the entire term 2. During the entire term 3. During the entire term

 

 

6. Contents

6.1. Units

- Unit 1. Prepositional and predicate logic's syntax and semantics
- Unit 2. Logic programming
- Unit 3. Program specification and formal verificationtext

6.2. Organization and concretion of contents 

Unit 1. Prepositional and predicate logic's syntax and semantics 

Concepts	Procedures	Behaviour
1. Propositional logic: logic connectors, formulas, truth tables, interpretations, satisfaction and validity, manipulation of formulas, semantic tableaux, natural deduction, resolution. 2. Predicate logic: quantifiers, formulas, interpretations, satisfaction and validity, semantic tableaux, natural deduction and resolution.	1. Be able to understand, specify and manipulate propositional formulas. Test the satisfaction and validity of propositional formulas. Apply methods like truth tables, semantic tableaux and resolution in specific problems. 2. Be able to understand, specify and manipulate predicate logic formulas. Test the satisfaction and validity of formulas. Apply methods like semantic tableaux and resolution to specific problems.	1. Appreciate the different types of useful formalisms in logic and reasoning. 2. Availability to try to understand concepts that initially seem complex.

Unit 2. Logic programming 

Concepts	Procedures	Behaviour
1. Clauses, programs, substitutions, unification.  2. SLD resolution, execution of logic programs.	1. Understand the relationship between formulas in logic and computational programs.  2. Describe the running process in logic programs. Implement different logic programs to solve specific problems.	1. Availability to try to understand concepts that initially seem complex. 2. Predisposition to acquire solid knowledge.

Unit 3. Program specification and formal verification 

Concepts	Procedures	Behaviour
1. Programming languages semantics 2. Formal specification of programs 3. Formal verification of programs	1. Define the formal semantics of imperative programs 2. Specify formally the programming semantics in specific problems. 3. Verify formally the correctness of specific programs.	1. Availability to try to understand concepts that initially seem complex. 2. Predisposition to acquire solid knowledge. 3. Availability to dedicate the necessary time to each concept.

7. Bibliography and teaching resources

7.1. Learning information resources. Basic bibliography (on paper or electronic media)

Mathematical Logic for Computer Science
Mordechai Ben-Ari
Springer (2003).

7.2. Learning information resources. Additional bibliography (on paper or electronic media)

Logic in Computer Science
Michael R.A. Huth, Mark D Ryan
Cambridge University Press (2002)

Logic and its Applications
Edmund Burke, Eric Foxley
Prentice Hall (1996)

7.3. Learning information resources. Reinforcement bibliography (on paper or electronic media)

7.4. Didactic resources. Subject learning material

Class' website
Notes/slides
Set of activities
Practical activities instructions

7.5. Didactic resources. Materials and tools.

SWI-Prolog self-extracting .EXE (3.75mb) 
Prolog Introductory Tutorial

8. Metodology

Methodological approach of the subject.
The usual learning process begins with a lecture where some theoretical and practical fundamentals are exposed. This activity is done with the whole group of students. Students must complement this activity with a careful reading of the notes and the additional material that the teacher provides. For example, a 2-hour lecture, properly used, will require an additional 1-hour work out of the classroom.
Then, the seminar sessions take place. In these sessions the students put into practice the concepts and techniques exposed in the lectures by solving small problems. For the first exercises of the session, the teacher will guide the solution, but not for the others. The aim is to consolidate the fundamentals so that later they can solve problems of greater complexity. For this activity the group is divided into four and it is performed in four small groups of students.
The next step in the learning process is the practical session. There, some larger problems that require integration of different concepts and techniques are proposed. The practical activities are incremental, each adding information to the previous practical activity. These activities are done in pairs and it is assumed that it continues out of the classroom.
The last step in the learning process of each unit is the resolution of autoevaluation activities. Through them, students can check if they have acquired the skills to be evaluated in the final exam.