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. (20-Nov-2009) M. Archer, B. Di Vito y César Muñoz Developing user strategies in PVS: A tutorial.

   Tutorial de M. Archer, B. Di Vito y César Muñoz sobre el desarrollo de estrategias en PVS.

2. (20-Nov-2009) A.L Galdino y M. Ayala A Theory for Abstract Reduction Systems in PVS.

   Artículo de A.L Galdino y M. Ayala que presenta una formalización de las reducciones abstractas en PVS análoga a la realizada en ACL2.

3. (10-Nov-2009) A. Darbari, B. Fischer y J. Marques-Silva Industrial-Strength Formally Certified SAT Solving.

   Demostración formal de un sistema SAT en Coq. El sistema extraido de la verificación es eficiente.

4. (8-Oct-2008) N. Sorensson Effective SAT solving

   Tesis de Septiembre de 2008.

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

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

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

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

7. (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.

3. ProofWeb

   ProofWeb es un sistema para construir demostraciones con orientación pedagógica a través de la Web. Está basado en Coq, aunque admite otros sistemas como Isabelle. Dispone de distintos tipos de presentación de las pruebas, como cálculo de secuentes y cajas de Fitch. Tiene una gran colección de ejercicios de ls cursos en que se ha usado.