Seminario del Grupo de Lógica Computacional

De WikiGLC
Revisión del 16:35 27 jun 2008 de Jalonso (discusión | contribuciones) (→‎Seminario del 14 de Julio de 2008)
Saltar a: navegación, buscar

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 14 de Julio de 2008

  • Título: El papel de ACL2 para incrementar la fiabilidad de Kenzo
  • Ponente:
Mirian Andrés
(Departamento de Matemáticas y Computación,
Universidad de La Rioja)
  • Resumen: La charla consiste en presentar de forma divulgativa una de las lineas de investigación de un grupo de la Universidad de La Rioja. Se explicarán los intereses en el uso de ACL2 y, de forma un poco más formal se mostrará, a modo de ejemplo, el trabajo Formalizing Simplicial Topology in ACL2 presentado en el pasado Workshop de ACL2 de 2007.

Seminario del 30 de Junio de 2008

Seminario del 23 de Junio de 2008

  • Título: Métodos formales: pasado, presente y futuro
  • Ponente: José A. Alonso
  • Resumen: En este seminario se comenta el estado actual de los métodos formales a partir de de las comunicaciones presentadas en Formal Methods Outreach Workshop (SRI 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.

Últimos añadidos

  1. (26-Jun-200) A.M. Frisch. W. Harvey, C. Jefferson, B. Martínez-Hernández Essence: A constraint language for specifying combinatorial problems.
    Essence is a formal language for specifying combinatorial problems in a manner similar to natural rigorous specifications that use a mixture of natural language and discrete mathematics. Essence provides a high level of abstraction, much of which is the consequence of the provision of decision variables whose values can be combinatorial objects, such as tuples, sets, multisets, relations, partitions and functions. Essence also allows these combinatorial objects to be nested to arbitrary depth, providing for example sets of partitions, sets of sets of partitions, and so forth. Therefore, a problem that requires finding a complex combinatorial object can be specified directly by using a decision variable whose type is precisely that combinatorial object.

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. S. Kieffer, J. Avigad y H. Friedman A language for mathematical language management.
    Presenta un lenguaje basado en ZFC para la representación práctica del conocimiento matemático. Más información en A language for mathematical knowledge management.
  4. A. Hommersom, P. J.F. Lucas y P. van Bommel Checking the Quality of Clinical Guidelines using Automated Reasoning Tools
    Aplicación del razonamiento automático (con OTTER/MACE) a la Medicina.
  5. 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.
  6. 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. H. Duncan The Use of Data-Mining for the Automatic Formation of Tactics.
    En esta tesis se presenta el NewT (New Tactic generator) y su implementación para Isabelle (el IsaNewT) que permite la construcción automática de tácticas usando técnicas del razonamiento probabilístico, aprendizaje automático y algoritmos genéticos. Ha sido dirigida por A. Bundy.
  4. 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.
  5. T. Weber SAT-based Finite Model Generation for Higher-Order Logic.
    En esta tesis de presenta una extensión de Isabelle/HOL que permite traducir las fórmulas a la lógica proposicional y usar SAT para buscar modelos. Está integrado en Isabelle como el método "refute".

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