Lògica a la Informàtica

• Professorat
• Hores setmanals
• Competències
• Objectius
• Continguts
• Activitats
• Metodologia docent
• Mètode d'avaluació
• Bibliografia
• Web links
• Capacitats prèvies

Professorat

Responsable

• Jose Miguel Rivero Almeida ( )

Altres

• Albert Atserias Peri ( )
• Antoni Lozano Boixadors ( )
• Enric Rodriguez Carbonell ( )

Hores setmanals

Competències

Competències Tècniques

Competències tècniques comunes

• CT1 - Demostrar coneixement i comprensió de fets essencials, conceptes, principis i teories relatives a la informàtica i a les seves disciplines de referència.
  • CT1.1A - Demostrar coneixement i comprensió dels conceptes fonamentals de la programació i de l'estructura bàsica d'un computador. CEFB4. Coneixement dels fonaments de l'ús i de la programació dels computadors, dels sistemes operatius, de les bases de dades i, en general, dels programes informàtics amb aplicació a l'enginyeria.
  • CT1.2C - Interpretar, seleccionar i valorar conceptes, teories, usos i desenvolupaments tecnològics relacionats amb la informàtica i la seva aplicació a partir dels fonaments matemàtics, estadístics i físics necessaris. CEFB3. Capacitat per a comprendre i dominar els conceptes bàsics de matemàtica discreta, lògica, algorísmica i complexitat computacional, i la seva aplicació per al tractament automàtic de la informació mitjançant sistemes computacionals i la seva aplicació per a la resolució de problemes propis de l'enginyeria.
• CT2 - Utilitzar d'una manera apropiada teories, procediments i eines en el desenvolupament professional de l'enginyeria informàtica en tots els seus àmbits (especificació, disseny, implementació, desplegament -implantació- i avaluació de productes) de manera que es demostri la comprensió dels compromisos adoptats a les decisions de disseny.
  • CT2.3 - Dissenyar, desenvolupar, seleccionar i avaluar aplicacions, sistemes i serveis informàtics i, al mateix temps, assegurar-ne la fiabilitat, la seguretat i la qualitat en funció de principis ètics i de la legislació i la normativa vigents.
• CT4 - Demostrar coneixement i capacitat d'aplicació dels procediments algorísmics bàsics de les tecnologies informàtiques per a dissenyar solucions a problemes, analitzant la idoneïtat i la complexitat dels algorismes
  • CT4.1 - Identificar les solucions algorísmiques més adequades per a resoldre problemes de dificultat mitjana.
  • CT4.2 - Raonar sobre la correcció i l'eficiència d'una solució algorísmica.
  • CT4.3 - Demostrar coneixement i capacitat d'aplicació dels principis fonamentals i de les tècniques bàsiques dels sistemes intel·ligents i de la seva aplicació pràctica.
• CT5 - Analitzar, dissenyar, construir i mantenir aplicacions de forma robusta, segura i eficient, triant el paradigma i els llenguatges de programació més adequats.
  • CT5.1 - Triar, combinar i explotar diferents paradigmes de programació, en el moment de construir software, tenint en compte criteris com la facilitat de desenvolupament, l'eficiència, la portabilitat i la mantenibilitat.
  • CT5.2 - Conèixer, dissenyar i utilitzar de forma eficient els tipus i les estructures de dades més adients per a la resolució d'un problema.
  • CT5.3 - Dissenyar, escriure, provar, depurar, documentar i mantenir codi en un llenguatge d'alt nivell per a resoldre problemes de programació aplicant esquemes algorísmics i utilitzant estructures de dades.
  • CT5.4 - Dissenyar l'arquitectura dels programes utilitzant tècniques d'orientació a objectes, de modularització i d'especificació i implementació de tipus abstractes de dades.

Competències Transversals

Raonament

• G9 [Avaluable] - Capacitat de raonament crític, lògic i matemàtic. Capacitat de resoldre problemes en la seva àrea d'estudi. Capacitat d'abstracció: capacitat de crear i utilitzar models que reflecteixin situacions reals. Capacitat de dissenyar i realitzar experiments senzills, i analitzar-ne i interpretar-ne els resultats. Capacitat d'anàlisi, de síntesi i d'avaluació.
  • G9.3 - Capacitat crítica, capacitat d'avaluació.

Tercera llengua

• G3 [Avaluable] - Conèixer l'idioma anglès amb un nivell adequat de forma oral i escrita, i en consonància amb les necessitats que tindran els graduats i les graduades en Enginyeria Informàtica. Capacitat de treballar en un grup multidisciplinar i en un entorn multilingüe i de comunicar, tant per escrit com de forma oral, coneixements, procediments, resultats i idees relacionats amb la professió d'enginyer tècnic en informàtica.
  • G3.2 - Estudiar amb materials escrits en anglès. Redactar un informe o un treball de tipus tècnic en anglès. Participar en una reunió tècnica en anglès.

Competències Tècniques de cada especialitat

Especialitat computació

• CCO1 - Tenir un coneixement profund dels principis fonamentals i dels models de la computació i saber-los aplicar per a interpretar, seleccionar, valorar, modelar i crear nous conceptes, teories, usos i desenvolupaments tecnològics, relacionats amb la informàtica.
  • CCO1.1 - Avaluar la complexitat computacional d'un problema, conèixer estratègies algorísmiques que puguin dur a la seva resolució, i recomanar, desenvolupar i implementar la que garanteixi el millor rendiment d'acord amb els requisits establerts.
• CCO2 - Desenvolupar de forma efectiva i eficient els algorismes i el software apropiats per a resoldre problemes complexos de computació.
  • CCO2.1 - Demostrar coneixement dels fonaments, dels paradigmes i de les tècniques pròpies dels sistemes intel·ligents, i analitzar, dissenyar i construir sistemes, serveis i aplicacions informàtiques que utilitzin aquestes tècniques en qualsevol àmbit d'aplicació.
  • CCO2.2 - Capacitat per a adquirir, obtenir, formalitzar i representar el coneixement humà d'una forma computable per a la resolució de problemes mitjançant un sistema informàtic en qualsevol àmbit d'aplicació, particularment en els que estan relacionats amb aspectes de computació, percepció i actuació en ambients o entorns intel·ligents.
• CCO3 - Desenvolupar les solucions informàtiques que, considerant l'entorn d'execució i l'arquitectura del computador sobre el qual s'executen, aconsegueixin el millor rendiment.
  • CCO3.1 - Implementar codi crític seguint criteris de temps d'execució, eficiència i seguretat.
  • CCO3.2 - Programar considerant l'arquitectura hardware, tant en asemblador com en alt nivell.

Objectius

1. Conéixer 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).
   Competències relacionades: G9.3, CCO2.1, CCO2.2,
2. Conéixer la definició (sintaxi i semàntica) de dues lògiques: la proposicional i la de primer ordre. Entendre, escriure i manipular ágilment fórmules en les dues lògiques, amb especial émfasi a les aplicacions a l'informàtica.
   
   Competències relacionades: G9.3, CCO2.1, CT4.1, CT4.2, CCO2.2, CT4.3,
3. Conéixer 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.
   Competències relacionades: G9.3, G3.2, CCO1.1, CCO2.1, CT4.1, CT4.2, CCO2.2, CT2.3,
4. Conéixer els mètodes de deducció per a determinar les propietats de l'objectiu previ de major relevància a la informàtica: Davis-Putnam, i resolució; la seva correcció i completesa respecte la definició de la lògica. Ser capaç d'aplicar a mà resolució i Davis-Putnam sobre exemples pràctics abordables, i saber utilitzar la resolució com a mecanisme de còmput (càlcul de respostes).
   Competències relacionades: G9.3, G3.2, CCO1.1, CCO2.1, CT4.1, CT4.2, CCO2.2, CT2.3,
5. Saber aplicar els fonaments lògics a algunes de les aplicacions, cada cop més abundants, a la informàtica dels mètodes deductius: fonaments de la programació lògica (Prolog), bases de dades deductives, circuits, problemes de planificació, etc. 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.
   Competències relacionades: G9.3, CT1.2C, G3.2, CCO1.1, CCO2.1, CT4.1, CT4.2, CT5.2, CT5.4, CCO2.2, CCO3.1, CCO3.2, CT4.3, CT5.1, CT5.3, CT1.1A, CT2.3,
6. Saber expressar problemes diversos utilitzant el llenguatge
   Prolog, i entendre les extensions "extra-lògiques" del Prolog
   incloses les dels diferents sistemes de restriccions.
   Competències relacionades: G9.3, G3.2, CCO2.1, CT4.1, CT4.2, CT5.2, CCO2.2, CCO3.1, CT4.3, CT5.1,

Continguts

1. Introducció i motivació:
   -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. Alguns exemples de problemes. Com els resoldríem amb les tècniques vistes a assignatures prèvies? Quant de temps ens costaria? Què en sabríem de les garanties de fiabilitat?
2. Definició de la Lògica Proposiciónal
   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ó sobre cost computacional polinòmic i exponencial (taules de veritat), cost lineal d'avaluar una fórmula, entre altres.
3. Deducció en Lògica Proposicional
   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 com utilitzar SAT solvers. Intuició sobre 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
   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
   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
   Càlcul de respostes: com trobar els valors de les variables X que fan que F satisfaci una expressió de la forma "Existeix X tal que 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.
   
7. Programació amb restriccions
   Com obtenir la flexibilitat i rapidesa en l'expressió del problema característica de la programació lògica, i a la vegada tenir l'eficiència de l'ús de resoledors especialitzats per als enters, els reals, dominis finits, etc.? CLP(X) i dominis. Maneres de reduir l'espai de cerca. Problemes lògics amb restriccions d"altres dominis. Exemple: assignació de recursos, horaris. Cerca de solucions òptimes amb CLP.

Activitats

Activitat Acte avaluatiu

Metodologia docent

Mètode d'avaluació

Bibliografia

Bàsica:

• Lógica para informáticos - Farré, R. [et al.], Marcombo, 2011. ISBN: 9788426716941
  https://discovery.upc.edu/discovery/fulldisplay?docid=alma991003857269706711&context=L&vid=34CSUC_UPC:VU1&lang=ca
• Logic for computer scientists - Schöning, U, Birkhäuser, 2008. ISBN: 9780817647636
  https://discovery.upc.edu/discovery/fulldisplay?docid=alma991001174279706711&context=L&vid=34CSUC_UPC:VU1&lang=ca

Complementaria:

• Handbook of constraint programming - Rossi, F.; van Beek, P.; Walsh, T, Elsevier , 2006. ISBN: 0444527264
  https://discovery.upc.edu/discovery/fulldisplay?docid=alma991003148729706711&context=L&vid=34CSUC_UPC:VU1&lang=ca
• Journal of the ACM (JACM) - Nieuwenhuis, Oliveras, Tinelli, , .
  http://cataleg.upc.edu/record=b1209995~S1*cat

Web links

• web principal de l'assignatura http://www.cs.upc.edu/~li

Capacitats prèvies