**LITI** Lógica Informática 2024-25 Ingeniería Informática - Tecnologías Informáticas Doble Grado Matemáticas - Informática # Ficha Técnica | | | |-|-| |Grado| [**Tecnologías Informáticas (Ingeniería en Informática)**](https://www.informatica.us.es/index.php/grados/tecnologias-informaticas)
[**Doble Grado en Matemáticas - Tecnologías Informáticas**](https://matematicas.us.es/titulaciones/doble-grado-informaticamatematicas/presentacion-del-doble-grado-informatica-y-matematicas)| |Profesores| [**Joaquín Borrego**](http://www.cs.us.es/~joaquin/), [**Andrés Cordón**](https://www.cs.us.es/perfiles/andres-cordon-franco), [**Fernando Sancho**](http://www.cs.us.es/~fsancho/)| |Tutorías| Consultar y acordar con el profesor del grupo correspondiente| # Contenido La primera pregunta que puede hacerse cualquier alumno de Informática al comenzar esta asignatura es: ¿por qué debería un informático aprender Lógica? Además de la labor de entrenamiento que supone aprender cualquier disciplina formal, podemos destacar, esencialmente, dos grandes vías para responder a esta pregunta: 1. En relación al modelado de tareas para automatizarlas computacionalmente (una de los usos más habituales de la computación hoy en día y de las labores más demandadas en un informático), es imprescindible conocer técnicas diversas del modelado y su aplicación de manera óptima y correcta. En esas tres tareas la Lógica juega un papel central. 2. Además, hay aplicaciones específicas relacionadas con la computación en las que la Lógica juega un papel fundamental: Descripción de semántica de lenguajes de programación; Corrección de sistemas y protocolos informáticos; Descripción del hardware informático; Razonamiento Automático; Modelado y Verificación de Sistemas Inteligentes; etc. Por ello, y dentro de la amplísima gama de técnicas que podemos encontrar en la Lógica, el objetivo específico de esta asignatura es el de estudiar la representación del conocimiento mediante **Lógica Proposicional (LP)** y **Lógica de Primer Orden (LPO)**, así como proponer métodos de razonamiento para cada una de ellas (como son los tableros semánticos y el método de resolución). Por ello, el contenido del curso se ha dividido en las siguientes unidades temáticas: | Lecturas | Transparencias | Ejercicios | |------------------------------|:------------------------------:|:------------------------:| | Tema 0. Introducción
- [Recurso 0.1: Breve Historia de la Lógica](Logica1.md.html) | | | | Tema 1: Sintaxis y Semántica de las Lógicas
- [Recurso 1.1: Sintaxis y Semántica LP](SintaxisSemanticaLP.md.html)
- [Recurso 1.2: Ejemplos resueltos formalización LP](FormalizacionLP.md.html)
- [Recurso 1.3: Sintáxis y Semántica LPO](SintaxisSemanticaLPO.md.html)
- [Recurso 1.4: Ejemplos resueltos formalización LPO](FormalizacionLPO.md.html) | [∀](.\recursos\tema-01.pdf) | [∃](.\recursos\rel01.pdf) | | Tema 2: Tableros Semánticos
- [Recurso 2.1: Tableros Semánticos en LP](TablerosLP.md.html)
- [Recurso 2.2: Tableros Semánticos en LPO](TablerosLPO.md.html) | [∀](.\recursos\tema-02.pdf) | [∃](.\recursos\rel02.pdf) | | Tema 3: [Formas Normales y Algoritmo DPLL](FormasNormalesDPLL.md.html) | [∀](.\recursos\tema-03.pdf) | [∃](.\recursos\rel03.pdf) | | Tema 4: [Formas Prenex, de Skolem y Teorema de Herbrand](PrenexSkolemHerbrand.md.html) | [∀](.\recursos\tema-04.pdf) | [∃](.\recursos\rel04.pdf) | | Tema 5: Resolución
- Recurso 5.1: [De la Resolución LP a la Resolución LPO](https://www.cs.us.es/~fsancho/Blog/posts/De_Resolucion_LP_a_LPO.md.html) | [∀](.\recursos\tema-05.pdf) | [∃](.\recursos\rel05.pdf) | | Tema 6: [Introducción a Prolog](https://www.cs.us.es/~fsancho/Blog/posts/Introduccion_Prolog.md.html) | [∀](.\recursos\tema-06.pdf) | [∃](.\recursos\rel06.pdf) | A lo largo del curso, el objetivo de las clases es presentar los fundamentos teóricos, realizar ejercicios seleccionados y responder dudas que puedan haber surgido durante la exposición del contenido. Cada tema dispone de un conjunto de **ejercicios** propuestos que son de realización aconsejable para una correcta asimilación de los conceptos teóricos introducidos, así como de sus aplicaciones prácticas. # Sistemas Aunque el curso está planteado principalmente como un curso teórico, en cuya ejecución no es necesario ningún sistema de implemetación ni software adicional, es indudable su relación con algunas herramientas computacionales (software) que se han desarrollado para aplicar su contenido o para ayudar a su compresión. Entre todo el software disponible, queremos destacar: * ![](.\img\logicuslogo.png align="right")[LogicUS](https://www.cs.us.es/~vramos/logicusWeb/). El sistema LogicUS está formado por tres herramientas  que proporcionan diferentes niveles de abstracción: **LogicUS-LIB** (motor funcional; bibliotecas funcionales programadas en Elm), **LogicUS-NB** (una integración con litvis para generar documentos ejecutables) y **LogicUS-GUI** (una interfaz GUI orientada a web y flujos ejecutables para su visualización e integración). La herramienta proporciona un sistema particularmente útil tanto en el contexto de la investigación (a través de una forma relativamente rápida, sencilla y  adaptable para la creación de prototipos basados en la lógica), como en el de la educación (a través de un marco que permite la ejecución de algoritmos a bajo nivel preservando las estructuras conceptuales y las metodologías subyacentes a los fundamentos lógicos). * ![](.\img\prover9.jpg align="right" width=200px)[Prover9 y Mace4](http://www.cs.unm.edu/~mccune/prover9/). Prover9 es un demostrador automático de teoremas para lógicas de primer orden (también puede ser usado para proposicional), y Mace4 busca modelos finitos y contraejemplos. En [esta entrada](http://www.cs.us.es/~fsancho/?e=173) puedes encontrar un pequeño manual de uso y algunos ejemplos básicos de cómo aplicarlo en problemas de LP y LPO. * ![](.\img\touuist.png align="right" width=100px)[TouIST](https://www.irit.fr/touist/): Un pequeño lenguaje de programación que permite expresar fórmulas proposicionales de una forma cómoda y natural. * [Prolog](https://www.swi-prolog.org/): Es un lenguaje de programación lógico e interpretado usado habitualmente en el campo de la Inteligencia artificial. * Algunas otras herramientas que pueden ser interesantes a lo largo del curso son: * [Gateway to Logic](https://www.erpelstolz.at/gateway/formular-uk.html): Permite realizar operaciones varias sobre fórmulas proposicionales (formas normales, tablas de verdad, árboles de formación, etc.). * [ProofTools](https://creativeandcritical.net/prooftools): Una aplicación para la generación automática y gráfica de Tableros Semánticos. Funciona, entre otras, para la LP, LPO y LPO con igualdad. * [Tree Proof Generator](http://www.umsu.de/logik/trees/): Genera Tableros Semánticos en LP y LPO. * [LogEx](http://ideas.cs.uu.nl/logex/): Convierte a formas normales y prueba equivalencias en LP. Se puede usar como herramienta de ejercicios porque permite la verificación de los pasos dados por el usuario, y también muestra la solución paso a paso. (Usa cualquier número como login). * [Logica](http://logica.stanford.edu/): Aplica el algoritmo UMG a dos expresiones. * [SATRennesPA](http://satrennespa.irisa.fr/WebContent/): Verificador de SAT para LP. * [Logictools](http://people.irisa.fr/Francois.Schwarzentruber/dpll_demo/): Un conjunto de librerías javascript para realizar diversos algoritmos (tablas de verdad, DPLL y resolución) para LP. El enlace lleva a una página preparado para probarlos. # Criterios de Evaluación ![](.\img\marking.jpg align="right" width=150)Se proporcionan dos métodos (no excluyentes entre sí) de aprobar la asignatura: * **Evaluación Continua**: Realizando a lo largo del cuatrimestre dos pruebas escritas de carácter obligatorio, una correspondiente a los temas 1 a 3, y otra a los temas 4 a 6. La media aritmética de estos dos exámenes será la nota asociada a la evaluación alternativa, y su superación permitirá aprobar la asignatura sin necesidad de realizar el examen final. Las fechas de estas pruebas serán anunciadas con suficiente antelación en esta misma página, y se realizarán en horas lectivas del curso y en cada grupo por separado. * **Convocatoria Oficial**: Mediante la superación de un examen final con todo el contenido del curso en las fechas previstas en el calendario de [Organización Docente de la E.T.S.I.I](https://www.informatica.us.es/index.php/calendario-de-examenes). A estos exámenes solo se podrán presentar los alumnos que no hayan superado la asignatura en la Evaluación Continua. # Bibliografía * Huth, M. y Ryan, M.: _Logic in Computer Science: Modelling and Reasoning about Systems_. Cambridge University Press, 2004. * Ben-Ari, M.: _Mathematical Logic for Computer Science_. Prentice Hall, 1993. * Davis, M.; Sigal, R.; Weyuker, E.: _Computability, complexity and languages_. Academic Press, 1994. * Doets, K.: _From Logic to Logic Programming_. MIT Press, 1994 * Poole, D.; Mackworth, A.; Goebel, R.: _Computational Intelligence_. Oxford University Press, 1998. * Russel, S.; Norvig, P.: _Inteligencia Artificial. Un enfoque moderno_. Pearson–Prentice Hall, 2003 (segunda edición). * Alonso, J.A.; Borrego, J.: [_Deducción automática (Vol. 1: Construcción lógica de sistemas lógicos)_](https://www.cs.us.es/~jalonso/publicaciones/2002-ded-automatica-1.pdf). Ed. Kronos, 2002. * Nilsson, U.; Maluszynski, J.: _Logic, Programming and Prolog_. John Willey and Sons Ltd., 1990.