Saltar al contingut Menu
Mapa
  • Inici
  • Informació
  • Contacte
  • Mapa

Introducció a la Lògica (IL)

Crèdits Dept. Tipus Requisits
7.5 (6.0 ECTS) CS-MA2
  • Obligatòria per a l'EI
  • Obligatòria per a l'ETIG
  • Obligatòria per a l'ETIS
   

Professors

Responsable:  (-)
Altres:(-)

Objectius Generals

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).

Objectius Específics

Coneixements

  1. El concepte de què és una lògica, en termes de sintaxi (què és una fórmula F), i semàntica (què és una interpretació I, i quan una I satisfà una F).
  2. La definició (sintaxi i semàntica) de dues lògiques: la proposicional i la de primer ordre.
  3. Els conceptes de tautologia/validesa, contradicció, conseqüència i equivalència lògiques (de forma independent de la lògica concreta), com s'utilitzen per a formalitzar problemes pràctics a l'informàtica, i com es redueixen al problema de satisfactibilitat.
  4. Els mètodes de deducció per a determinar aquestes propietats de major relevància a la informàtica: Davis-Putnam, i resolució; la seva correcció i completesa respecte de la definició de la lògica.
  5. El poder expressiu de les dues lògiques, i entendre en quin sentit la lògica proposicional és una restricció de l'altra; compromís entre poder expressiu i bones propietats computacionals: primeres nocions intuïtives de complexitat i decidibilitat.
  6. Algunes de les -cada cop més abundants- aplicacions a la informàtica dels mètodes deductius: fonaments de la programació lògica (Prolog), bases de dades deductives, circuits, problemes de planificació, etc.

Habilitats

  1. Entendre, escriure i manipular ágilment fórmules en les dues lògiques, amb especial émfasi a les aplicacions a l'informàtica.
  2. Saber demostrar formalment propietats senzilles sobre fórmules, conjunts, relacions, funcions, etc, mitjançant tècniques de demostració com ara el contrarrecíproc, contraexemeple, inducció, o reducció l'absurd.
  3. Ser capaç d'aplicar a ma resolució i Davis-Putnam sobre exemples pràctics abordables, i saber utilitzar la resolució com a mecanisme de còmput (càlcul de respostes).
  4. Saber expressar alguns problemes pràctics NP-complets (sudokus, horaris, problemes de grafs, circuits) com a problemes de satisfacció de lògica proposicional, i resoldre-ls amb un SAT solver.
  5. Saber expressar problemes senzills utilitzant el llenguatge Prolog, i entendre les extensions "extra-lògiques" del Prolog (l'aritmética predefinida, l'operador de tall i la negació, l'entrada/sortida).

Competències

(Informació no introduïda)

Continguts

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

1. Introducció i motivació
T      P      L      Alt    L Ext. Est    A Ext. Total 
2,0 0 0 0 0 2,0 0 4,0
-Importància de la lògica a la informàtica, exemples
-Lògica informàtica vs lògica matemàtica
-Què és una lògica
-Objectius de l'assignatura

2. Definició de la Lògica Proposiciónal
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.
  • Laboratori:
    Nota: no es fa distinció entre classes de teoria i de problemes.

3. Deducció en Lògica Proposicional
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)

4. Definició de la Lògica de Primer Ordre
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.

5. Deducció en Lògica de Primer Ordre
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ó.

6. Programació Lògica
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

Metodologia docent

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.

Mètode d'avaluació

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.

Bibliografía bàsica

  • Uwe Schöning Logic for computer scientists, Birkhäuser, 1989.
  • María Teresa Hortalá González, Javier Leach Albert, Mario Rodríguez Artalejo Matemática discreta y lógica matemática, Complutense, 2001.

Bibliografía complementària

(Informació no introduïda)

Enllaços web

(Informació no introduïda)

Capacitats prèvies

Introducció a la programació i a la programació recursiva.


Compartir

 
logo FIB © Facultat d'Informàtica de Barcelona - Contacte - RSS
Aquest web utilitza cookies pròpies per oferir una millor experiència i servei. En continuar amb la navegació entenem que acceptes la nostra política de cookies.
Versió clàssica Versió mòbil