Person in charge: | (-) |
Others: | (-) |
Credits | Dept. | Type | Requirements |
---|---|---|---|
7.5 (6.0 ECTS) | CS-MA2 |
|
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.
-Davis-Putnam-Logemann-Loveland algorithm (DPLL) (from truth tables and decision trees), The explicit stack of Backtracking -How to express problems in SAT and use SAT-solvers -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 -First-order 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 -No-termination: decision procedures and (co-)semi-decision 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 extra-logic aspects: negation, predefined arithmetic, input-output. 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
first-order 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.