I1M2012: Presentación del curso de “Informática (de 1º de Matemáticas)

PorJosé A. Alonso

En la clase de hoy del curso Informática (de 1º de Grado en Matemáticas) se ha presentado la asignatura siguiendo el resumen del proyecto docente y los materiales en la página de la asignatura:

Se ha explicado cómo instalar los sistemas y se ha mostrado una sesión sobre el uso de Haskell y emacs. La sesión está grabada en este vídeo.

Se ha comentado el sistema de evaluación y se ha anunciado las fechas de los exámenes de todo el curso.

LI2012: Lógica y programación

PorJosé A. Alonso

En la primera parte de la clase de hoy Lógica Informática se ha comentado las relaciones entre la lógica y la programación. Se han mostrado un programa con una máquina de Turing, un programa en Prolog y un demostrador proposicional en Haskell.

En la segunda parte he comentando relaciones entre las lógicas e informática:

  • la de primer orden con la programación lógica (que verán en la signatura de “Programación declarativa”),
  • la de orden superior con la verificación de sistemas (que verán en la asignatura de “Razonamiento asistido por computador”),
  • las modales con los agentes inteligentes (que verán en la asignatura de “Sistemas inteligentes”)
  • las descriptivas con la Web semántica (que verá en la asignatura de “Representación del conocimiento en la Web”).

Reseña: Mechanization of an algorithm for deciding KAT terms equivalence

PorJosé A. Alonso

Se ha publicado un nuevo trabajo sobre verificación formal en Coq: Mechanization of an algorithm for deciding KAT terms equivalence.

Sus autores son Nelma Moreira, David Pereira y Simao Melo de Sousa (de la Universidade do Porto, Portugal).

Su resumen es

This work presents a mechanically verified implementation of an algorithm for deciding the (in-)equivalence of Kleene algebra with tests (KAT) terms. This mechanization was carried out in the Coq proof assistant. The algorithm decides KAT terms equivalence through an iterated process of testing the equivalence of their partial derivatives. It is a purely syntactical decision procedure and so, it does not construct the underlying automata. The motivation for this work comes from the possibility of using KAT encoding of propositional Hoare logic for reasoning about the partial correctness of imperative programs.

El código de la formalización en Coq se encuentra aquí.

Reseña: Lifting and transfer: A modular design for quotients in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un nuevo artículo sobre automatización del razonamiento en Isabelle/HOL: Lifting and transfer: A modular design for quotients in Isabelle/HOL.

Sus autores son Brian Huffman y Ondřej Kunčar (de la Technische Universität München).

El trabajo se presentará el 12 de agosto en el Isabelle Users Workshop 2012 en el marco del ITP 2012 (third conference on Interactive Theorem Proving).

Su resumen es

Quotients, subtypes, and other forms of type abstraction are ubiquitous in formal reasoning with higher-order logic. Typically, users want to build a library of operations and theorems about an abstract type, but they want to write definitions and proofs in terms of a more concrete representation type, or “raw” type. Earlier work on the Isabelle Quotient package [1, 2] has yielded great progress in automation, but it still has many technical limitations.

We present an improved, modular design centered around two new packages: the Transfer package for proving theorems, and the Lifting package for defining constants. Our new design is simpler, applicable in more situations, and has more user-friendly automation. An initial implementation is available in Isabelle 2012.

Reseña: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization

PorJosé A. Alonso

Esta semana se ha publicado en el Journal of Automated Reasoning un nuevo artículo de razonamiento formalizado en PVS: Formalization of an efficient representation of Bernstein polynomials and applications to global optimization. Una versión previa se puede leer libremente aquí.

Los autores son César Muñoz y Anthony Narkawicz de NASA Langley Formal Methods.

Su resumen es

This paper presents a formalization in higher-order logic of an efficient representation of multivariate Bernstein polynomials. Using this representation, an algorithm for finding lower and upper bounds of the minimum and maximum values of a polynomial has been formalized and verified correct in the Prototype Verification System (PVS). The algorithm is used in the definition of proof strategies for formally and automatically solving polynomial global optimization problems.