Profesorado

Francisco Palomo Lozano (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

- Investigación de desastres reales provocados por fallos en sistemas
críticos.
- Búsqueda de rompecabezas lógicos para su resolución con SATO y Prover9.
- Modelado de un sistema mediante una máquina de estados finita para su
comprobación con SAL.
- Programación de funciones en ACL2.

Metodología

Se empleará una metodología cuyo objetivo es lograr el aprendizaje a
través de la resolución de problemas. Las clases correspondientes a los
créditos teóricos constarán, fundamentalmente, de sesiones de resolución
de problemas propuestos con antelación en las que los alumnos podrán
emplear cuantos materiales estimen convenientes.

Los alumnos deberán primero intentar resolver los problemas por sí mismos,
para luego trabajar por parejas, explicándose mutuamente la solución
obtenida e intentando encontrar errores en la solución del compañero, o
bien, intentando llegar juntos a una solución. Posteriormente, las
soluciones se pondrán en común en grupo y se invitará a su exposición. El
objetivo es fomentar el trabajo cooperativo, el espíritu crítico y la
comunicación.

Se hará especial hincapié en la necesidad de comprobar la corrección de la
solución final obtenida y su bondad respecto a distintos criterios, al
objeto de fomentar el espíritu crítico.

El profesor enseñará los conocimientos teóricos y técnicos necesarios bajo
demanda, conforme los alumnos los requieran para resolver los problemas
planteados, limitándose a actuar de guía en el proceso de aprendizaje. El
alumno es responsable de su propio aprendizaje.

No obstante, el profesor realizará al principio de cada tema una breve
introducción de sus aspectos principales y de dónde encontrar información
adicional, proporcionando diversos materiales a lo largo del curso.

Dado el enfoque eminentemente práctico que se desea imprimir a la
asignatura, las clases teóricas y las prácticas se entremezclarán y, de
hecho, ambas clases se impartirán en el laboratorio. Se proporcionarán
ejercicios que se desarrollarán en clase a lo largo del curso.

Las clases se servirán del campus virtual como apoyo para la  docencia.
Estarán disponibles herramientas de comunicación como foros
especializados, tutorías electrónicas privadas y correo electrónico, así
como diversos contenidos en formato digital.

Distribución de horas de trabajo del alumno/a

Nº de Horas (indicar total): 100

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

Técnicas Docentes

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.

El alumno podrá superar la asignatura mediante evaluación continua, a
través de la entrega de trabajos durante el curso. En tal caso, la nota
final será la media de las notas obtenidas en cada uno de los trabajos
propuestos.

No obstante, también es posible asistir a las convocatorias de exámenes
finales que establecen los Estatutos de la Universidad de Cádiz. A este
efecto, la asignatura se evaluará mediante un examen final realizado en el
laboratorio y la nota final será exclusivamente la obtenida en él.

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.