"Razonamiento Automático" es una asignatura obligatoria del 2º curso del Grado en Inteligencia Artificial, que se imparte durante el 2º cuatrimestre.



En esta asignatura, se presentan las bases formales de:

A) El razonamiento lógico: razonar es la capacidad de hacer inferencias sobre un conocimiento dado, y el razonamiento automático se refiere a la construcción y uso de sistemas informáticos que automatizan este proceso.

B) La representación del conocimiento: se consideran las dos lógicas clásicas más utilizadas, lógica proposicional y lógica de primer orden.

Además, se utiliza de manera práctica el software de razonamiento automático disponible a día de hoy y se analizan las aplicaciones importantes en Inteligencia Artificial.



De esta manera, se profundiza y completan los conocimientos introducidos en asignaturas del 1er curso del grado. Concretamente:



1) En la asignatura "Matemática Discreta", donde se presentan algunos sistemas de razonamiento deductivos para lógica proposicional y lógica de primer orden.

2) En la asignatura "Metodología de la Programación", donde se utiliza lógica de primer orden como lenguaje de especificación formal.



Junto con esta asignatura, durante el 2º cuatrimestre del 2º curso del grado se imparten otras dos asignaturas, "Bases de Datos" e "Inteligencia Artificial", en las que también se trata el problema de la representación del conocimiento, aunque desde otras perspectivas. Además, en la asignatura "Inteligencia Artificial" también se estudian otros métodos de razonamiento, como pueden ser los sistemas basados en reglas.



El conocimiento que se presenta en esta asignatura sirve de base o se completa en asignaturas de cursos superiores del grado, como pueden ser "Diseño de Bases de Datos" (3º), "Desarrollo de Aplicaciones Big Data" (3º), "Sistemas Basados en el Conocimiento" (4º) o "Técnicas Avanzadas de Inteligencia Artificial" (4º).

* Representar conocimiento usando lenguajes lógicos formales.

* Demostrar formalmente que una conclusión se deduce de una premisa utilizando sistemas formales automatizables.

* Construir modelos y contra-modelos de enunciados lógicos.

* Entender los algoritmos y estrategias que se utilizan en la deducción automática.

* Manejar distintas herramientas automáticas de razonamiento y entender los resultados que producen.

1. Representación matemática del conocimiento.

2. Métodos y herramientas de deducción en lógica proposicional.

3. Métodos y herramientas de deducción en lógica de primer orden.

4. Aplicaciones del razonamiento automático en Inteligencia Artificial: Prolog.

En la modalidad magistral se expondrán los contenidos conceptuales de la asignatura y se realizarán ejercicios o problemas prácticos acerca de los mismos.



Asimismo, durante las prácticas de laboratorio se resolverán ejercicios o problemas prácticos adicionales mediante la utilización de herramientas automáticas disponibles.



En ambos casos, se utilizarán metodologías activas que propicien que el alumnado adquiera competencias trabajando tanto de forma autónoma como en equipo para resolver los distintos objetivos propuestos. Además, se fomentará la formulación de cuestiones y su discusión, de tal manera que el alumnado adquiera destrezas relacionadas con la comunicación oral, la capacidad de síntesis y el trabajo en equipo.



Para facilitar y asegurar el aprendizaje del alumnado, se hará un seguimiento y se proporcionará feed-back en base a criterios de evaluación previamente establecidos, de tal manera que tengan la oportunidad de tomar conciencia acerca de su progresión.

• Sistema de Evaluación Continua
• Sistema de Evaluación Final
• Herramientas y porcentajes de calificación:
  • Los porcentajes y tipos de evaluación se especifican en los apartados siguientes. (%): 100

Se seguirán los criterios establecidos en la normativa vigente para la elección del sistema de evaluación (continua o final), y también para los cambios de sistema de evaluación (de continua a final).



===Evaluación continua===



La evaluación continua engloba la evaluación de los conocimientos y destrezas adquiridas mediante la realización de exámenes parciales (70%) y la entrega de ejercicios o problemas prácticos resueltos (30%).



En concreto, se realizarán 3 exámenes parciales, en los que se evaluará respectivamente los siguientes apartados y con el siguiente porcentaje sobre la calificación final de la asignatura:

* 1er examen parcial: Lógica proposicional, 20%.

* 2º examen parcial: Lógica de primer orden, 25%.

* 3er examen parcial: Aplicaciones prácticas - Prolog, 25%.



Todas las pruebas de evaluación se evaluarán con una nota comprendida entre 0 y 10 puntos.



La calificación final de la asignatura se obtendrá como la media ponderada de las notas obtenidas en los exámenes parciales y los ejercicios/problemas entregados.



En todo caso, para aprobar la asignatura será necesario obtener:

a) Una calificación mínima de 3 puntos en cada examen parcial.

b) Una calificación final mínima de 5 puntos.



===Evaluación final===



La evaluación se realiza mediante un único examen escrito que supone el 100% de la calificación final de la asignatura, comprendida entre 0 y 10 puntos.



Será necesario obtener una calificación final mínima de 5 puntos para aprobar la asignatura.



No realizar el examen escrito de la evaluación final se considerará como renuncia a la evaluación.

Se seguirán los mismos criterios aplicados en la modalidad de evaluación final de la convocatoria ordinaria.



Es decir, la evaluación se realiza mediante un único examen escrito que supone el 100% de la calificación final de la asignatura, comprendida entre 0 y 10 puntos.



Será necesario obtener una calificación final mínima de 5 puntos para aprobar la asignatura.



No realizar el examen escrito de la evaluación final se considerará como renuncia a la evaluación.

El material disponible en el aula virtual (eGela) de la asignatura.

Bibliografía básica

"Logic for Computer Scientists". Uwe Schöning. Volume 8 in the series "Progress in Computer Science and Applied Logic". 166 pages. Birkhäuser, 1989. ISBN: 9780817647629. e-ISBN: 13:978-0-8176-4763-6. DOI: 10.1007/978-0-8176-4763-6. Springer, 2008 (reprint).



"Introduction to Logic, Third Edition". Michael Genesereth and Eric J. Kao. Volume 5(1) in the series "Synthesis Lectures on Computer Science". 177 pages. Morgan & Claypool, 2016.ISSN: 1932-1228 (print) 1932-1686 (electronic). DOI: 10.2200/S00734ED2V01Y201609CSL008. Online resources available at: http://intrologic.stanford.edu/

Bibliografía de profundización

"Handbook of Automated Reasoning". Alan Robinson and Andrei Voronkov (editors). 981 pages (Volume I), 1185 (Volume II). The MIT Press (North-Holland), 2001. ISBN: 9780262182218 (Volume I), ISBN: 9780262182225 (Volume II), ISBN: 9780262182232 (Volumes I and II).

Revistas

* Journal of Automated Reasoning (https://www.springer.com/journal/10817/)

* Journal of Logic and Computation (https://academic.oup.com/logcom)

* ACM Transactions on Computational Logic (https://dl.acm.org/journal/tocl)

* The Journal of Logic and Algebraic Programming (https://www.sciencedirect.com/journal/the-journal-of-logic-and-algebraic-programming)

Direcciones web

The TPTP Problem Library for Automated Theorem Proving:
http://www.tptp.org/
System on TPTP:
http://www.tptp.org/cgi-bin/SystemOnTPTP
The CADE ATP System Competition:
http://tptp.org/CASC/

Logic Tools:
http://logictools.org/