Francisco Palomo Lozano (coordinador)

Al término de la asignatura el alumno deberá:

- Reconocer la importancia de automatizar el razonamiento
- Emplear herramientas lógicas para modelar problemas complejos
- Emplear a nivel elemental sistemas de razonamiento automatizado
- Verificar programas simples con ayuda de un sistema de este tipo

Teoría:

1. Introducción (2h)
1.1. Tipos de razonamiento
1.2. Necesidad de automatizar el razonamiento
1.3. Aplicaciones

2. Automatización del razonamiento lógico (10h)
2.1. Lógica clásica
2.2. Decidibilidad, indecidibilidad y semidecidibilidad
2.3. Completitud e incompletitud
2.4. Procedimientos de decisión

3. Automatización del razonamiento ecuacional (3h)
3.1. Lógica ecuacional
3.2. Reescritura de términos
3.3. Terminación y confluencia

4. Aplicaciones a la verificación de software (10h)
4.1. Lógica computacional
4.2. Introducción a ACL2
4.3. Aplicaciones industriales

Prácticas:

1. Resolución de problemas lógicos con SATO (2h)
1.1. Formato de cláusulas DIMACS
1.2. Resolución del problema de las 8 damas
1.3. Coloreo de un mapa

2. Implementación del algoritmo DPLL (10h)
2.1. Analizador
2.2. Estructuras de datos
2.3. Reglas DPLL
2.4. Motor de inferencia
2.5. Pruebas

3. Verificación de un programa sencillo con ACL2 (8h)
3.1. Comprobación de si una lista está ordenada
3.2. Inserción de un elemento en una listas ordenada
3.3. Eliminación de un elemento en una lista ordenada
3.4. Comprobación de si una lista es permutación de otra
3.5. Ordenación de listas

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.

Las clases prácticas complementan los contenidos de la parte teórica. Se
proporcionarán ejercicios que se desarrollarán en el laboratorio a lo largo del
curso.

Tanto las clases teóricas como las prácticas 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.

Nº de Horas (indicar total): 100

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

Se emplearán como técnicas de evaluación exámenes y trabajos.

Como criterios de evaluación de 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.

- Bibliografía básica

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

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

[3] J. Harrison
Introduction to Logic and Automated Theorem Proving.
Cambridge University Press (2007)

[4] M. Kaufmann, P. Manolios, J S. Moore.
Computer-Aided Reasoning: An Approach.
Kluwer Academic Publishers (2000)

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

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

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

- Bibliografía complementaria

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

[2] D. Kelley.
The Art of Reasoning.
W. W. Norton & Company. 3ª ed. (1998)

[3] L. Wos y G. W. Pieper.
A Fascinating Country in the World of Computing.
World Scientific (2000)