Seminario del Grupo de Lógica Computacional

Los Seminarios del Grupo de Lógica Computacional se celebrarán los lunes de 10:00 a 11:00 en el seminario del módulo L4 del Departamento de Ciencias de la Computación e Inteligencia Artificial.

Seminarios del curso 2007-08

Seminario del 5 de Mayo de 2008

• Título: Patrones básicos de razonamiento en Isabelle/Isar
• Ponente: José A. Alonso
• Resumen: En este seminario se presentan los patrones básicos de Isabelle/Isar para el razonamiento proposicional, cuantificacional e inductivo. Se pondrá el énfasis en las demostraciones estructuradas. El contenido del seminario se corresponde con los capítulos 2 y 3 de Introduccion a la demostracion asistida por ordenador (con Isabelle/Isar).

---

Seminario del 28 de Abril de 2008

• Título: Isabelle como lenguaje de programación e Isar como lenguaje de demostración
• Ponente: José A. Alonso
• Resumen: Este seminario es el primero de una serie cuyo objetivo es mostrar las posibilidades de Isabelle/Isar como sistema que permite regular el nivel de automatización de las demostraciones y hacerlas legibles por los humanos y procesable por las máquinas. El contenido del seminario se corresponde con los dos primeros capítulos de Introduccion a la demostracion asistida por ordenador (con Isabelle/Isar).

---

Material de interés para el Seminario del GLC

En la siguiente lista se recoge una relación de materiales que sería interesante comentar en el Seminario.

Representación del conocimiento y razonamiento

1. N. Leone, G. Pfeifer, W. Faber, T. Eiter, G. Gottlob, S. Perri y F. Scarcello

The DLV System for Knowledge Representation and Reasoning.

1. Presenta la metodología de resolución de problemas basada en conjuntos de problemas en uno de sus principales sistemas.

2. C. Baral [www.cs.ualberta.ca/~you/courses/621-01/chitta.ps Knowledge Representation, Reasoning and Declarative Problem Solving].

   Es el libro básico sobre programación basada en conjunto de respuestas.

Automatización del razonamiento

1. J.A. Navarro Encoding and Solving Problems in Effectively Propositional Logic.

   Es una tesis reciente sobre implementación y aplicaciones de SAT. Ha sido dirigida por Voronkov y se ha presentado el año 2007.

Sistemas para la enseñanza de la lógica

1. APLI2

   APLI2 (APLIcación de Ayuda Para Lógica Informática) es una herramienta para ayudar en el aprendizaje de la representación del conocimento en lógica de primer orden.

2. ProofBuilder

   ProofBuilder es un sistema para construir demostraciones con orientación pedagógica.

                     e

Caminante, no hay camino:
se hace camino al andar.
(A. Machado)

Con cada paso que das alcanzas tu meta.
(Dicho Zen).