Responsable: | (-) |
Altres: | (-) |
Crèdits | Dept. | Tipus | Requisits |
---|---|---|---|
7.5 (6.0 ECTS) | CS-MA2 |
|
Responsable: | (-) |
Altres: | (-) |
L'objectiu d'aquesta assignatura és proporcionar a l'estudiant una base sòlida de coneixements teòrics i pràctics de lògica per informàtics, i, al mateix temps, contribuir a la seva formació global en raonament formal (sobre conjunts, relacions, funcions, estructures d'ordre, recursió, comptatge), i tècniques de demostració (contrarrecíproc, contraexemples, inducció, reducció a l'absurd).
Hores estimades de:
T | P | L | Alt | L Ext. | Est | A Ext. |
Teoria | Problemes | Laboratori | Altres activitats | Laboratori extern | Estudi | Altres hores fora d'horari fixat |
|
T | P | L | Alt | L Ext. | Est | A Ext. | Total | ||
---|---|---|---|---|---|---|---|---|---|---|
12,0 | 0 | 0 | 0 | 0 | 12,0 | 0 | 24,0 | |||
-Sintaxi i semàntica de la LP
-Satisfacció, tautologia, conseqüència i equivalència -Tots aquests problemes es poden expressar com a SAT -Poder expressiu: quines coses es poden modelar Exercicis sobre: inducció, llegibilitat única de fórmules, formalització de problemes, comptatge (de fórmules, interpretacions, etc.), problemes de conseqüència i equivalència lògiques, intuició de cost computacional polinòmic vs. exponencial (taules de veritat), cost lineal d'avaluar una fórmula, entre altres.
|
|
T | P | L | Alt | L Ext. | Est | A Ext. | Total | ||
---|---|---|---|---|---|---|---|---|---|---|
12,0 | 0 | 0 | 0 | 0 | 12,0 | 0 | 24,0 | |||
-Formes normals, literals i clàusules.
-Algorisme de Davis-Putnam-Logemann-Loveland (DPLL) (a partir de taules de veritat i arbres de decisió), La pila explícita de Backtracking -Com expressar problemes com a SAT, i utilitzar SAT-solvers -Intuició de problemes NP i NP complets -Sistemes deductius: propietats de correctesa, completesa, i completesa refutacional. -Resolució: clausura sota resolució. Exercicis sobre formes normals, cost de les transformacions, relació amb circuits digitals, deducció per resolució i DPLL, i formulació de problemes com a SAT: (sudokus, vertex cover, confecció d'horaris, hitting set) |
|
T | P | L | Alt | L Ext. | Est | A Ext. | Total | ||
---|---|---|---|---|---|---|---|---|---|---|
15,0 | 0 | 0 | 0 | 0 | 15,0 | 0 | 30,0 | |||
-Sintaxi i semàntica de la LPO
-Fórmules tancades -Poder expressiu i decidibilitat -La LP com a cas particular de la LPO -Lògica de primer ordre amb igualtat i teories Exercicis sobre: llegibilitat única de fórmules, formalització de problemes, comptatge (de fórmules, interpretacions, etc.), problemes de conseqüència i equivalència lògiques, models finits i infinits,etc. |
|
T | P | L | Alt | L Ext. | Est | A Ext. | Total | ||
---|---|---|---|---|---|---|---|---|---|---|
15,0 | 0 | 0 | 0 | 0 | 15,0 | 0 | 30,0 | |||
-Formes normals, literals i clàusules.
-Pas a forma clausal, Skolemització -Unificació, unificador simultani, les regles d'unificació: acabament i correcció. -Resolució i factorització: correctesa i completesa refutacional -No-terminació: procediments de decisió i de (co-)semi-decisió Exercicis de formalització, pas a forma clausal, unificació, resolució, i problemes sobre (semi-)decisió aplicats als programes i la compilació. |
|
T | P | L | Alt | L Ext. | Est | A Ext. | Total | ||
---|---|---|---|---|---|---|---|---|---|---|
14,0 | 0 | 0 | 0 | 0 | 14,0 | 0 | 28,0 | |||
-Càlcul de respostes: com trobar els valors de X que fan que F\models \exists X G?
-L'estratègia SLD de resolució per clàusules de Horn -Completesa pel càlcul de respostes -La pila de backtracking: què fa l'operador de tall? -Altres aspectes extra-lògics: la negació, l'aritmètica predefinida, l'entrada-sortida. Exercicis de resolució amb càlcul de respostes, sobre la teoria i el comportament de programes Prolog, i de confecció de programes Prolog. |
Total per tipus | T | P | L | Alt | L Ext. | Est | A Ext. | Total |
70,0 | 0 | 0 | 0 | 0 | 70,0 | 0 | 140,0 | |
Hores addicionals dedicades a l'avaluació | 0 | |||||||
Total hores de treball per l'estudiant | 140,0 |
A les sessions de classe (en total cinc hores setmanals) s'intercalaran teoria i problemes de manera flexible segons les necessitats del temari a cada moment. No convé fixar de manera rígida quantes i quines hores setmanals seran de problemes. No hi ha classes de laboratori.
La metodologia docent es basa en els següents principis:
1. Es planteja la classe com un inici de l'estudi i el treball que l'estudiant ha de continuar i aprofundir pel seu compte.
2. Es proporciona el màxim de materials de qualitat (apunts, exercicis resolts, exercicis per fer, referències bibliogràfiques).
3. S'aprofiten al màxim les classes per a fomentar la motivació de l'estudiant (amb exemples, debats, comentaris, etc.) i es transmet l'enfocament i les intuïcions darrere les definicions, propietats i tècniques tractades.
Al voltant de la setmana 7 del quadrimestre es farà un parcial d'uns 90 minuts de duració, sobre els dos temes de lògica proposicional, amb un pes del 40% de la nota total.
L'examen final, a celebrar a l'epoca de exàmens, tindrà dues parts: recuperació dels dos temes de lògica proposicional (40% de la nota final) i els temes de lògica de primer ordre i programació lògica (60%). Tot estudiant pot decidir lliurement si es presenta o no a la part de recuperació, i se li comptarà la nota màxima entre la nota d'aquesta part i el parcial, és a dir, inclús si té una nota molt alta, no corre el risc de perdre-la.
Els exàmens constaran de preguntes de comprensió dels conceptes, de demostració de propietats, d'aplicació de les tècniques de deducció, i de resolució de problemes Prolog.
Qualsevol intent de frau realitzat durant el curs comportarà l'aplicació de la normativa acadèmica general de la UPC i l'inici d'un procés disciplinari.
Introducció a la programació i a la programació recursiva.