Person in charge:  () 
Others:  () 
Credits  Dept.  Type  Requirements 

7.5 (6.0 ECTS)  CSMA2 

Person in charge:  () 
Others:  () 
The aim of this course is to provide a solid basis of theoretical and practical knowledge on logic for computer scientists, and, at the same time, to contribute to the students' global education in formal reasoning (on sets, relations, functions, orders, recursion and counting) and proof techniques (counter example, induction, by contradiction).
Estimated time (hours):
T  P  L  Alt  Ext. L  Stu  A. time 
Theory  Problems  Laboratory  Other activities  External Laboratory  Study  Additional time 

T  P  L  Alt  Ext. L  Stu  A. time  Total  

12,0  0  0  0  0  12,0  0  24,0  
Syntax and Semantics of Propositional Logic
Satisfaction, validity, consequence and equivalence All these notions can be expressed as SAT Expressive power: which things can be modeled Exercises on: induction, unique readability of formulas, formalization of problems, counting (of formulas, interpretations, etc.), problems on logical consequence and equivalence, intuitions on polynomial vs. exponential computational costs (truth tables), linear time evaluation of formulas, among others.


T  P  L  Alt  Ext. L  Stu  A. time  Total  

12,0  0  0  0  0  12,0  0  24,0  
 Normal forms, literals and clauses.
DavisPutnamLogemannLoveland algorithm (DPLL) (from truth tables and decision trees), The explicit stack of Backtracking How to express problems in SAT and use SATsolvers Intuition of NP and NP complete problems Deductive systems: properties of correctness, completeness and refutational completeness. Resolution: closure under resolution. Exercises on normal forms, cost of the transformations, relationship with digital circuits, deduction by resolution and DPLL, and formulation of problems in SAT: (sudokus, vertex cover, planning, hitting set) 

T  P  L  Alt  Ext. L  Stu  A. time  Total  

15,0  0  0  0  0  15,0  0  30,0  
Sintax and semantics of LPO
Closed formulas Expressive power and decidability LP as a particular case of LPO Firstorder logics with equality and theories Exercises on: unique legibility of formulas, formalitzation of problems, counting (of formulas, interpretations, etc.), problems of logic consequence and equivalence, finite and infinite models,etc. 

T  P  L  Alt  Ext. L  Stu  A. time  Total  

15,0  0  0  0  0  15,0  0  30,0  
Normal forms, literals and clauses.
Clause form transformation, Skolemitzation Unification, simultaneous unifier, unification rules: termination and correctness. Resolution and factorization: correctness and refutational completeness Notermination: decision procedures and (co)semidecision procedures Exercises on formalitzation, clause form transformation, unification, resolution, and (semi)decision problems applied to programs and compilation. 

T  P  L  Alt  Ext. L  Stu  A. time  Total  

14,0  0  0  0  0  14,0  0  28,0  
Answer computation: how to find the values of X that satisfy F\models \exists X G?
 SLD resolution for Horn clauses Completeness for answer computation The backtracking stack: what does the cut operator do? Other extralogic aspects: negation, predefined arithmetic, inputoutput. Exercises on resolution with answer computation, on theory and the behavior of Prolog programs, and the implementation of Prolog programs. 
Total per kind  T  P  L  Alt  Ext. L  Stu  A. time  Total 
70,0  0  0  0  0  70,0  0  140,0  
Avaluation additional hours  0  
Total work hours for student  140,0 
Theory and problems will be interleaved during the lectures (a total of five hours per week), depending on the needs at each moment. It is not convenient to rigidly define which and how many hours per week will be problem sessions. There are no lab sessions.
The methodology is based on the following principles:
1. The lecture is a starting point for the student's independent study and work.
2. As many as possible materials will be provided (lecture notes, solved exercises, unsolved ones, bibliographical references).
3. Lectures will be exploited for motivation (with examples, debates, commments, etc.) and intuition behind the applied definitions, properties and techniques will be given.
Around the week 7 of the quatrimester an exam of around 90 minutes will be taken, on the two main propositional logic chapters, with a weight of 40% of the final grade.
The final exam, which will take place during the exams period, will have two parts: on the two main propositional logic chapters (with a weight of 40%) and on
firstorder logic and logic programming (60%). Any student can freely decide whether or not to do
the first part.
The propositional logic grade will be the maximum of the one obtained in the partial exam and this part of the final exam. That is, even if the grade of the partial exam is very high, there is no risk of losing it.
The exams will consist of questions on understanding of the concepts, on proving propoerties, on applying deduction techniques, and solving Prolog problems.
Any attempt of fraud during the course will entail the application of the UPC's general academic normative and the beginning of a disciplinary process.
Introduction to the programme and recursive programming.