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

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). La modalidad de evaluación por defecto es evaluación continua. De hecho, la asignatura está orientada a la modalidad de evaluación continua.



=== 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 ===



Se podrá solicitar el cambio de evaluación continua a evaluación final siempre y cuando no se haya evaluado un porcentaje igual o superior al 80% de la calificación final de la asignatura.



La evaluación final de la asignatura 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)