Profesorado

Alberto Salguero Hidalgo (coordinador)

Situación

Prerrequisitos

Ninguno

Contexto dentro de la titulación

Esta asignatura muestra cómo formalizar procesos de razonamiento con
diversos grados de automatización. En otras asignaturas, algunos de estos
procesos suelen abordarse desde un punto de vista informal y resolverse
manualmente, otros son simplemente inabordables.

Fundamentalmente, se trata de resolver problemas de manera lógica y
aplicar estas soluciones en campos tan importantes para un Ingeniero en
Informática como la verificación de software y hardware.

Lejos de ser una asignatura meramente teórica, se presentan numerosos
casos reales de problemas y aplicaciones industriales.

Recomendaciones

Aunque no es en absoluto imprescindible, los alumnos que hayan cursado
previamente asignaturas de Inteligencia Artificial, Programación Lógica y
Programación Funcional se beneficiarán de los conocimientos adquiridos
en ellas, apreciando mejor las ventajas que ofrecen los métodos y técnicas
tratadas.

Competencias

Competencias transversales/genéricas

- Análisis y síntesis.
- Razonamiento abstracto.
- Pensamiento crítico.
- Resolución de problemas.
- Comunicación y trabajo en equipo.
- Expresión oral y escrita.
- Preparación y presentación de documentación técnica.

Competencias específicas

• Cognitivas(Saber):

  - Conocer la naturaleza de los sistemas críticos, donde los errores
  pueden producir graves daños a personas y bienes.
  - Conocer ejemplos reales de sistemas críticos.
  - Conocer qué es y por qué es necesario automatizar el razonamiento.
  - Conocer sus aplicaciones a la resolución de problemas lógicos.
  - Conocer sus aplicaciones industriales.
  - Conocer sus limitaciones teóricas y prácticas.
  

• Procedimentales/Instrumentales(Saber hacer):

  - Modelar problemas complejos mediante distintas lógicas.
  - Reducir problemas de un dominio a otro.
  - Programar un sistema de razonamiento lógico sencillo.
  - Emplear sistemas de razonamiento especializados.
  - Resolver diversos problemas con la ayuda de  estos sistemas.
  

• Actitudinales:

  - Ser consciente de la responsabilidad que se asume en un sistema
  crítico.
  - Apreciar la necesidad y las ventajas de la automatización del
  razonamiento.
  - Valorar la importancia de consultar con soltura bibliografía y
  otros materiales en lengua inglesa.
  - Estar dispuesto a buscar y contrastar información de diversas
  fuentes de manera independiente.
  - Ser consciente de la necesidad de abordar nuevos problemas y
  evaluar posibles soluciones con espíritu crítico.
  - Apreciar las ventajas de trabajar cooperativamente en pequeños
  grupos, comunicando ideas con claridad y rigor.

Objetivos

Adquirir las competencias específicas reseñadas.

Programa

Teoría:

1. Introducción.
1.1. Sistemas críticos.
1.2. Necesidad de automatizar el razonamiento.
1.3. La máquina de radioterapia Therac 25.
1.4. La línea Meteor del metro de París.

2. Automatización del razonamiento lógico.
2.1. Lógica clásica.
2.2. Fragmentos notables.
2.3. Procedimientos de decisión.
2.4. Introducción a los sistemas SATO y Prover9.
2.5. Aplicaciones industriales.

3. Comprobación de modelos.
3.1. Lógicas temporales.
3.2. Introducción al sistema SAL.
3.3. Aplicaciones industriales.

4. Verificación.
4.1. Lógicas computacionales.
4.2. Introducción al sistema ACL2.
4.3. Aplicaciones industriales.

5. Limitaciones teóricas y prácticas.
5.1. Indecidibilidad.
5.2. Incompletitud.
5.3. Complejidad.

Prácticas:

1. Programación del algoritmo DPLL.
1.1. Analizador.
1.2. Estructuras de datos.
1.3. Reglas DPLL y motor de inferencia.
1.4. Pruebas.

2. Resolución de problemas lógicos con SATO.
2.1. Formato de cláusulas DIMACS.
2.2. Coloreo de mapas.
2.3. Resolución de Sudokus.
2.4. Equivalencia de circuitos digitales combinacionales.

3. Modelado y comprobación de modelos con SAL.
3.1. Modelado de una red de comunicaciones.
3.2. Modelado del protocolo de autenticación de Needham-Schroeder.
3.3. Síntesis automática de un escenario de ataque.

4. Programación y verificación de software con ACL2
4.1. Listas ordenadas y permutaciones.
4.2. Inserción y eliminación en listas ordenadas.
4.3. Ordenación de listas.

Actividades

Distribución de horas de trabajo del alumno/a

Nº de Horas (indicar total): 100

• Clases Teóricas:  
• Clases Prácticas:  
• Exposiciones y Seminarios:  
• Tutorías Especializadas (presenciales o virtuales):
  • Colectivas:  
  • Individules:  
• Realización de Actividades Académicas Dirigidas:
  • Con presencia del profesorado:  
  • Sin presencia del profesorado:  
• Otro Trabajo Personal Autónomo:
  • Horas de estudio:  
  • Preparación de Trabajo Personal:  
  • ...
     
• Realización de Exámenes:
  • Examen escrito: 1  
  • Exámenes orales (control del Trabajo Personal):  

Criterios y Sistemas de Evaluación

Como criterios de evaluación se tendrán en cuenta la claridad, elegancia y
eficiencia de las soluciones obtenidas. Se valorará especialmente la
capacidad del alumno para explicar con claridad el proceso por el cual
obtiene la solución al problema.

La asignatura se evaluará mediante un examen final realizado en el
laboratorio y la nota final será exclusivamente la obtenida en él.

Al dejar de impartirse la asignatura en el curso 2014/2015 dispone de 4
convocatorias de examen que puede distribuir durante los cursos 2014/2015 y
2015/2016

Recursos Bibliográficos

- Bibliografía básica.

[1] Fitting, M.
First-Order Logic and Automated Theorem Proving.
Springer. 2ª ed. 1995.

[2] Harrison, J.
Handbook of Practical Logic and Automated Reasoning.
Cambridge University Press. 2009.

[3] Kaufmann, M.; Manolios, P. y Moore, J S.
Computer-Aided Reasoning: An Approach.
Kluwer Academic Publishers. 2000.

[4] Monin, J.-F.
Understanding Formal Methods.
Springer. 2003.

[5] Wos, L.; Overbeek, R.; Lusk, R. y Boyle, J.
Automated Reasoning: Introduction and Applications.
McGraw-Hill. 2ª ed. 1992.

- Bibliografía complementaria.

[1] Baader, F. y Nipkow, T.
Term Rewriting and All That.
Cambridge University Press. 1998.

[2] Baier, C. y Katoen, J.-P.
Principles of Model Checking.
MIT Press. 2008.

[3] Clark, E. M.; Grumberg, O. y Peled, D. A.
Model Checking.
MIT Press. 2000.

[4] Hortalá González, T.; Palomino Tarjuelo, M.;Martí Oliet, N. y
Rodríguez Artalejo, M.
Lógica Matemática para Informáticos. Ejercicios Resueltos.
Pearson. 2008.

[5] Julián Irazo, P. y Alpuente Fresnedo, M.
Programación Lógica. Teoría y Práctica.
Pearson. 2007.

[6] Kaufmann, M.; Manolios, P. y Moore, J S.
Computer-Aided Reasoning: ACL2 Case Studies.
Kluwer Academic Publishers. 2000.

[7] Kelley, D.
The Art of Reasoning.
W. W. Norton & Company. 3ª ed. 1998.

[8] Schöning, U.
Logic for Computer Scientists.
Modern Birkhäuser Classics. Birkhäuser. 2008.

[9] Smullyan, R. M.
First-Order Logic.
Dover Publications. 1995.

[10] Wos, L. y Pieper, G. W.
A Fascinating Country in the World of Computing.
World Scientific. 2000.

- Bibliografía especializada de consulta.

[1] Robinson, J. A. y Voronkov, A. (ed.)
Handbook of Automated Reasoning.
MIT Press. 2001.