Seminario del Grupo de Lógica Computacional

Los Seminarios del Grupo de Lógica Computacional se celebrarán los miércoles de 12:00 a 13: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.

Próximos seminarios

Seminario del 15 de Octubre de 2008

• Título: La regla de independencia y su aplicación al aprendizaje de atributos
• Ponente: Joaquín Borrego
• Resumen: En esta charla presentaremos una nueva regla de inferencia, de carácter proposicicional (la regla de independencia). Se mostrará una aplicación de dicha regla al aprendizaje de atributos en el Análisis Formal de Conceptos

---

Seminarios anteriores

En esta sección se encuentran los seminarios de los cursos anteriores.

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. (8-Oct-2008) N. Sorensson Effective SAT solving

   Tesis de Septiembre de 2008.

2. (18-Sep-2008) vdash.org

   Es un proyecto de una wiki con conocimiento matemático formalizado en Isabelle/Isar.

3. (11-Sep-2008) N. Shankar The Verified Software Initiative

   Presenta ideas para un ambicioso proyecto internacional sobre verificación de programas.

4. (26-Jun-2008) 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).