José A. Alonso Jiménez

Informática (1º del Grado en Matemáticas):

Esta asignatura es una introducción a la programación funcional con Haskell y su aplicación a la algorítmica y a la resolución de problemas matemáticos. También se estudia el cálculo simbólico con Maxima. Las páginas de los cursos en los que he impartido la asignatura son: 2009-10, 2010-11, 2011-12, 2012-13, 2013-14, 2014-14, 2015-16, 2016-17, 2017-18, 2018-19 y 2019-20.

Programación declarativa (3º de Ingeniería Informática)

Esta asignatura es una introducción a la programación declarativa en su doble aspecto: programación funcional con Haskell y programación lógica con Prolog. El contenido del curso ha evolucionado desde usar sólo Prolog (en los cursos 1999-00, 2000-01, 2001-02, 2002-03, 2003-04, 2004-05, 2005-06 y 2006-07) para ir aumentando el uso de Haskell (en los cursos 2007-08, 2008-09 y 2009-10).

Programación lógica (Doctorado)

En esa asignatura se estudia la programación lógica desde un punto de vista aplicado. Se comienza con la presentación de Prolog como un sistema deductivo y como lenguaje de programación. A continuación se estudia aplicaciones de la programación lógica en inteligencia artificial. Finalmente, se estudian extensiones de la programación lógica. Las páginas de los cursos en los que he impartido la asignatura son: 2002-03, 2003-04, 2004-05 y 2008-09.

Informática (1º de Diplomatura en Estadística)

Esta asignatura es una introducción a la programación usando Scheme. Las páginas de los cursos en los que he impartido la asignatura son: 1997-98.

Lógica informática (2º del Grado en Ingeniería Informática)

Este curso es una introducción de los principales conceptos lógicos tanto de la lógica proposicional como de la de primer orden. Para ambas se consideran distintos cálculos y procedimientos de decisión. Las páginas de los cursos en los que he impartido la asignatura son: 2003-04, 2004-05, 2005-06, 2006-07, 2007-08, 2008-09, 2009-10, 2010-11, 2011-12, 2012-13, 2013-14, 2014-15 y 2015-16.

Lógica y programación (3º de Ingeniería Informática).

En esta asigntura se estudian e implementan en Lisp distintos procedimientos lógicos: sintaxis y semántica proposicional, formas normales y cláusulas, el procedimiento de Davis-Putnam, la resolución proposicional e intérpretes de Prolog. También se estudian cómo resolver problemas con el demostrador de teoremas Otter. La página del curso en el que he impartido la asignatura es 1999-00.

Lógica matemática y fundamentos (3º del Grado en Matemáticas)

En el curso se estudia la sintaxis, semántica de la lógica proposicional y de primer orden. Como sistema deductivos en ambas lógicas se estudia la deducción natural y cómo se construyen dichas demostraciones con Isabelle/HOL. También se estudia la programación funcional en Isabelle/HOL y se demuestran formalmente propiedades de dichos programas. Finalmente se estudia el desarrollo formal de teorías con Isabelle/HOL. Las páginas de los cursos en los que he impartido la asignatura son: 2011-12, 2012-13, 2013-14, 2014-15, 2015-16, 2016-17, 2017-18. 2018-19 y 2019-20.

Seminario de lógica computacional (Doctorado).

En este asignatura se estudia los fundamentos lógicos de la programación lógica. Las páginas de los cursos en los que he impartido la asignatura son: 1991-92, 1995-96 y 1996-97.

Razonamiento automático (Máster Universitario en Lógica, Computación e Inteligencia Artificial)

Esta asignatura es una introducción al razonamiento automático asistido por ordenador usando Isabelle/HOL y Coq. Las páginas de los cursos en los que he impartido la asignatura son: 2010-11, 2011-12, 2012-13, 2013-14, 2014-15, 2015-16, 2016-17, 2017-18, 2018-19 y 2019-20.

Demostración automática de teoremas

Es una asignatura de libre configuración para la Licenciatura de Matemáticas en la que se estudia la demostración automática de teoremas con Otter. Las páginas de los cursos en los que he impartido la asignatura son: 2002-03, 2003-04 y 2004-05.

Razonamiento automático (5º de Ingeniería Informática).

En esta asignatura se estudia el razonamiento automático por resolución en Otter y se implementa sistemas de razonamiento con Prolog. Los sistemas usados en los cursos ha ido cambiado: con Lisp y Nqthm (el 1998-99) y con Otter y Prolog los siguientes (1999-00, 2000-01, 2001-02 y 2002-04).

Métodos formales en computación e I.A (Doctorado).

En este curso se estudian los métodos formales usando el sistema de razonamiento PVS. Las páginas de los cursos en los que he impartido la asignatura son: 2001-02 y 2002-03.

Representación del conocimiento y razonamiento

Esta asignatura es una introducción a la representación del conocimiento y razonamiento. Las páginas de los cursos en los que he impartido la asignatura son: 2006-07 y 2007-08.

Inteligencia artificial I (4º de Ingeniería Informática).

En esta asignatura se estudia la representación de problemas mediante espacio de estados y su resolución mediante búsquedas, las heurísticas en juegos y la representación lógica del conocimiento y su razonamiento. La implementaciones se hacen con Lisp y Prolog. Las páginas de los cursos en los que he impartido la asignatura son: 1997-98, 1998-99 y 1999-00.

Inteligencia artificial II (4º de Ingeniería Informática).

En este curso se estudia la programación basada en reglas con CLIPS y Prolog. Concretamente se estudian la construcción de metaintérpretes, el procesamiento de lenguaje natural, razonamiento con redes semánticas y marcos, razonamiento por defecto y aprendizaje automático. Las páginas de los cursos en los que he impartido la asignatura son: 1997-98, 1998-99, 1999-00, 2000-01, 2001-02 y 2002-03.

Heurística y sistemas expertos (3º de Licenciatura en Estadística).

En este curso se estudia la programación con reglas usando CLIPS y su aplicación para construir sistemas expertos. También se estudia Maxima como sistema experto en Matemáticas. La página del curso en el que he impartido la asignatura es 1996-97.