Diferencia entre revisiones de «Seminario del Grupo de Lógica Computacional»

De WikiGLC
Saltar a: navegación, buscar
(→‎Automatización del razonamiento)
(→‎Automatización del razonamiento)
Línea 66: Línea 66:
  
 
=== Automatización del razonamiento ===
 
=== Automatización del razonamiento ===
 +
# S. Berghofer [http://mediatum2.ub.tum.de/doc/601727/document.pdf Proofs, Programs and Executable Specifications in Higher Order Logic].
 +
#: En esta tesis se explica cómo extraer programas evaluables a partir de especificaciones en Isabelle/Isar.
 
# A. Chaieb [http://mediatum2.ub.tum.de/doc/649541/document.pdf Automated methods for formal proofs in simple arithmetics and algebra].
 
# A. Chaieb [http://mediatum2.ub.tum.de/doc/649541/document.pdf Automated methods for formal proofs in simple arithmetics and algebra].
 
#: En esta tesis se estudia cómo integrar métodos de razonamiento en demostradores de la familia LCF.
 
#: En esta tesis se estudia cómo integrar métodos de razonamiento en demostradores de la familia LCF.

Revisión del 14:13 21 jun 2008

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. Las sesiones son abiertas y pueden acudir todas las personas interesadas.

Seminarios del curso 2007-08

Seminario del 23 de Junio de 2008

Seminario del 16 de Junio de 2008

  • Título: Sensor-IA
  • Ponente: Francisco J. Martín
  • Resumen: Se realizará una presentación del proyecto "Sensor-IA" realizado para el Instituto Andaluz de Tecnología.

Seminario del 9 de Junio de 2008

Seminario del 26 de Mayo de 2008

Seminario del 19 de Mayo de 2008

  • Título: APLI2: pasado, presente y futuro.
  • Ponente: Gonzalo A. Aranda-Corral
  • Resumen: APLI2 es un sistema desarollado para la ayuda a la enseñanza de la Lógica. En esta charla describiremos tanto la arquitectura del sistema como usabilidad y posibles ampliaciones del sistema.

Seminario del 12 de Mayo de 2008

Seminario del 5 de Mayo de 2008

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 esta sección 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.
    Presenta la metodología de resolución de problemas basada en conjuntos de problemas en uno de sus principales sistemas.
  2. C. Baral Knowledge Representation, Reasoning and Declarative Problem Solving.
    Es el libro básico sobre programación basada en conjunto de respuestas.
  3. Arjen Hommersom, Peter J.F. Lucas y Patrick van Bommel Checking the Quality of Clinical Guidelines using Automated Reasoning Tools
    Aplicación del razonamiento automático (con OTTER/MACE) a la Medicina.
  4. A. Paskevych Méthodes de formalisation des connaissances et des raisonnements mathématiques: aspects appliqués et théoriques
    En esta tesis se presenta el sistema SAD que permite el pocesamiento semántico de textos matemáticos.
  5. D. Walukiewicz-Chrzaszcz y J. Chrzaszcz Consistency and Completeness of Rewriting in the Calculus of Constructions
    Resumen: Adding rewriting to a proof assistant based on the Curry-Howard isomorphism, such as Coq, may greatly improve usability of the tool. Unfortunately adding an arbitrary set of rewrite rules may render the underlying formal system undecidable and inconsistent. While ways to ensure termination and confluence, and hence decidability of type-checking, have already been studied to some extent, logical consistency has got little attention so far. In this paper we show that consistency is a consequence of canonicity, which in turn follows from the assumption that all functions defined by rewrite rules are complete. We provide a sound and terminating, but necessarily incomplete algorithm to verify this property. The algorithm accepts all definitions that follow dependent pattern matching schemes presented by Coquand and studied by McBride in his PhD thesis. It also accepts many definitions by rewriting, containing rules which depart from standard pattern matching.

Automatización del razonamiento

  1. S. Berghofer Proofs, Programs and Executable Specifications in Higher Order Logic.
    En esta tesis se explica cómo extraer programas evaluables a partir de especificaciones en Isabelle/Isar.
  2. A. Chaieb Automated methods for formal proofs in simple arithmetics and algebra.
    En esta tesis se estudia cómo integrar métodos de razonamiento en demostradores de la familia LCF.
  3. 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.


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

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

Obtenido de «https://www.glc.us.es/web/index.php?title=Seminario_del_Grupo_de_Lógica_Computacional&oldid=102»