Ver el código de «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 ===
# (20-Nov-2009) M. Archer, B. Di Vito y César Muñoz [http://www.cs.odu.edu/~mln/casi/20030067563_2003080659.pdf 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. 
# (20-Nov-2009) A.L Galdino y M. Ayala [http://www.mat.unb.br/~ayala/ARS.pdf 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. 
# (10-Nov-2009) A. Darbari, B. Fischer y J. Marques-Silva [http://arxiv.org/abs/0911.1678 Industrial-Strength Formally Certified SAT Solving].
#: Demostración formal de un sistema SAT en Coq. El sistema extraido de la verificación es eficiente.
# (8-Oct-2008) N. Sorensson [http://gupea.ub.gu.se/dspace/bitstream/2077/18263/1/gupea_2077_18263_1.pdf Effective SAT solving]
#: Tesis de Septiembre de 2008.
# (18-Sep-2008) [http://vdash.org/ vdash.org]
#: Es un proyecto de una wiki con conocimiento matemático formalizado en Isabelle/Isar.
# (11-Sep-2008) N. Shankar [http://qpq.csl.sri.com/vsr/vsi.pdf The Verified Software Initiative]
#: Presenta ideas para un ambicioso proyecto internacional sobre verificación de programas.  
# (26-Jun-2008) A.M. Frisch. W. Harvey, C. Jefferson, B. Martínez-Hernández [http://www.springerlink.com/content/11u842537916v570/ 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 ===
# N. Leone, G. Pfeifer, W. Faber, T. Eiter, G. Gottlob, S. Perri y F. Scarcello [http://arxiv.org/abs/cs/0211004v2 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. 
# C. Baral [http://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.
# S. Kieffer, J. Avigad y H. Friedman [http://arxiv.org/abs/0805.1386 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 [http://www.andrew.cmu.edu/user/avigad/Papers/mkm/index.html A language for mathematical knowledge management].
# A. Hommersom, P. J.F. Lucas y P. van Bommel [http://arxiv.org/abs/0806.0250 Checking the Quality of Clinical Guidelines using Automated Reasoning Tools]
#: Aplicación del razonamiento automático (con OTTER/MACE) a la Medicina.
# A. Paskevych [http://tertium.feechki.org/papers/thesis-07.fr.pdf 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.
# D. Walukiewicz-Chrzaszcz y J. Chrzaszcz [http://arxiv.org/abs/0806.1749 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 ===
# 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].
#: En esta tesis se estudia cómo integrar métodos de razonamiento en demostradores de la familia LCF.
# H. Duncan [http://www.era.lib.ed.ac.uk/bitstream/1842/1768/1/hazelthesis.pdf 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.
# J.A. Navarro [http://www.mpi-sws.mpg.de/~jnavarro/papers/phdthesis.pdf 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.
# T. Weber [http://www4.in.tum.de/~webertj/publications/weber08satbased.pdf 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 ===
# [http://www.glc.us.es/~jalonso/apli2 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.
# [http://www.cis.gvsu.edu/~mcguire/ProofBuilder/ ProofBuilder]
#: ProofBuilder es un sistema para construir demostraciones con orientación pedagógica.
# [http://proofweb.cs.ru.nl 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.