Profesorado

Inmaculada Medina Bulo  (coordinadora)
Francisco Palomo Lozano

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] 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.

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

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

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

[6] Schöning, U.
Logic for Computer Scientists.
Birkäuser. 1989.

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

[8] 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.