Contextualització

Dades de la matèria

Any acadèmic
2011-12
Nom
LÒGICA COMPUTACIONAL
Codi Assignatura/Matèria
102004
Centre
Escola Politècnica Superior
Departament
INFORMATICA I ENGINYERIA INDUSTRIAL
Cicle
1
Tipologia
TRONCAL
Extensió
1R Q AVALUACIO CONTINUADA
Crèdits ECTS
6.0
Hores
150.0
Percentatge d'ús de l'Idioma
Idioma
Percentatge d'ús
Català
50.0
Anglès
0.0
Castellà
50.0

Recomanacions (màx. 4000 caràcters)

Enviar un correu electrònic als professors per a qualsevol dubte i/o qüestió.

Assignatura/matèria en el conjunt del pla d'estudis (màx. 4000 caràcters)

Assignatura que s'imparteix durant el primer semestre del primer curs de la titulació. 
Correspon a la Matèria "Informàtica" dins del Mòdul de "Formació Bàsica".

Requisits per cursar-la

Prerequisits
Corequisits

Professorat

Nom
Correu
Horari de consulta
Crèdits teòrics
Crèdits pràctics
Maria Teresa Alsinet Bernadó
tracy@diei.udl.cat
Dijous i divendres de 12:00 a 13:30
5.4
Carlos Jose Ansotegui Gil
carlos@diei.udl.cat
5.4

Competències

Competències estratègiques de la Universitat de Lleida

  • Domini de les Tecnologies de la Informació i la Comunicació.
    Objectius
    • Utilitzar un SAT solver. Utilitzar un entorn de desenvolupament de programes lògics basat en un intèrpret de prolog.

Competències específiques de la titulació

  • Capacitat per comprendre i dominar els conceptes bàsics de matemàtica discreta, lògica, algorísmica i complexitat computacional, i la seva aplicació per a la resolució de problemes propis de l'enginyeria.
    Objectius
    • Modelitzar enunciats en el llenguatge formal de la lògica proposicional.
    • Raonar sobre la validesa de les formules en lògica proposicional.
    • Aplicar sistemes de demostració automàtica per a les formules de la lògica proposicional.
    • Modelitzar enunciats en el llenguatge formal de la lògica de primer ordre.
    • Raonar sobre la validesa de les formules de la lògica de primer ordre.
    • Aplicar sistemes de demostració automàtica per a la lògica de primer ordre.
    • Aplicar els fonaments de la programació declarativa.
    • Aplicar els sistemes lògics de raonament automàtic de la lògica proposicional i de primer ordre per a la resolució de problemes de l'enginyeria informàtica i les matemàtiques.

Competències transversals de la titulació

  • Capacitat per a l'abstracció i el raonament crític, lògic i matemàtic.
    Objectius
    • Modelitzar enunciats mitjançant llenguatges formals. Raonar sobre la validessa de les fòrmules lògiques. Raonar sobre els procediments de prova. Aplicar sistemes de demostració automàtica basats en els procediments de prova.
  • Capacitat de resolució de problemes i elaboració i defensa d'arguments dins de la seva àrea d'estudis.
    Objectius
    • Modelitzar enunciats en els llenguatges formals de la lògica matemàtica. Identificar el millor formalisme lògic en funció de la caracterització de l'enunciat. Raonar sobre la validesa de les fòrmules lògiques. Automatització dels sistemes de prova.

Continguts

Continguts de la matèria

El programa de l'assignatura s'estructura en els temessegüents:

 Tema  1:  Introducció als Sistemes Lògics i Raonament Automàtic
 Tema  2:  Lògica Proposicional
 Tema  3:  Lògica de Primer Ordre
 Tema  4:  Programació Lògica
 
Tema 2: Lògica Proposicional:

  • Sintaxi,  Semàntica i Taules de veritat
  • Classificació d'enunciats (satisfactible, insatisfactible i tautologia)
  • Equivalència lògica,  Equisatisfactibilitat i Conseqüència lògica 
  • Modelització d'enunciats
  • Transformació a Formes Normals: Forma Clausal
  • Principi de Resolució
  • Demostració automàtica de la validesa d'enunciats


 Tema 3:  Lògica de Primer Ordre:

  • Sintaxi  i Semàntica
  • Classificació d'enunciats (satisfactible, insatisfactible i tautologia)
  • Equivalència lògica
  • Modelització d'enunciats
  • Substitució, Composició de substitucions i  Aplicació de substitucions a expressions
  • Unificador d'expressions i unificador més general
  • Transformació a Formes Normals: Forma Clausal
  • Principi de Resolució
  • Demostració automàtica de la validesa d'enunciats

 

Tema  4:  Programació Lògica

  • Programes Lògics
  • Resolució SLD
  • Introducció a Prolog

Bibliografia

Bibliografia recomanada

Bàsica

  • Teresa Hortalá, Narciso Martí, Miguel Palomino, Mario Rodríguez, Rafael del Vado. Lógica matemática par informáticos. Pearson, Prentice Hall, 2008.
  • Paniagua E., Sánchez J.L. y Martín F.: Lógica Computacional. Thomson-Paraninfo, 2003.
  • J. Leach and M. Rodríguez-Artalejo. Lógica Matemática. Notas del Curso. Facultad deMatemáticas. Universidad Complutense, Madrid, 1992.
  • C.L. Changand and R.C.T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, Inc., 1973.
  • J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, second edition, 1987.
  •  F. Manyà. Notes de Lògica DIEI - Universitat de Lleida, 2004.
  •  U. Schöning. Logic forComputer Scientists. Birkhäuser, Boston, 1989.

Programació Lògica i Prolog

  •  Pascual Julián Iranzo and María Alpuente Frasnedo. Programación Lógica: Teoría y Práctica Pearson PrenticeHall, 2007.
  • W. Clocksin and C. Mellish.Programming in Prolog. Springer-Verlag, 1981.
  • I. Bratko. Prolog Programming for Artificial Intelligence (2nd. ed.). Addison-Wesley, 1990.
  • Sterling y Shapiro: The Art of Prolog. MIT Press, 1994.
Bibliografia complementària

  • Chang-Lee: Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
  • Gallier, J.: Logic for Computer Science: Foundations of AutomaticTheorem Proving, 2003. (http://www.cis.upenn.edu/~jean/gbooks/logic.html)
  • Genessereth: Logical Foundations of Artificial Intelligence. Genessereth and Nilsson, Morgan Kaufmann Publishers, 1987.
  • Cuena, J.: Lógica Informática TOMO II: Lógica Computacional. Publicaciones FIM, 1999.
  • Tymoczko T. and Henle J.: Razón, dulce razón. Una Guía de Campo de la Lógica Moderna. Ariel, 2002.