Menu Close

Etiqueta: Isabelle/HOL

RA2018: Razonamiento por casos y por inducción en Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático hemos profundizado en el estudio de las demostraciones por casos y por inducción. En concreto, se ha estudiado

  • el razonamiento por casos booleanos,
  • el razonamiento por casos booleanos sobre una variable,
  • el razonamiento por casos sobre listas,
  • el razonamiento por inducción sobre números naturales con patrones,
  • el razonamiento sobre definiciones con existenciales,
  • el uso de librerías auxiliares (como Parity) y
  • el uso de otros métodos de demostración (como presburg).

La teoría con los ejemplos presentados en la clase es la siguiente:

RA2018: Razonamiento estructurado sobre programas con Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL.

Para ello, se ha visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 8 del curso de Informática.

Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.

La teoría con los ejemplos presentados en la clase es la siguiente:

RA2018: Razonamiento automático sobre programas en Isabelle/HOL

En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de los ejercicios de la 1ª relación.

En la segunda parte, se ha estudiado cómo se pueden demostrar manualmente propiedades de programas Haskell. Para ello, se han usado las transparencias del tema 8 del curso de Informática (de 1º del Grado en Matemática). Como lectura complementaria se recomienda el capítulo 13 del libro de G. Hutton Programming in Haskell.

A continuación se ha explicado cómo demostrar automáticamente las propiedades anteriores con Isabelle/HOL.

El enunciado de las propiedades es inmediato: basta escribir la palabra lemma y a continuación la propiedad entre comillas dobles; por ejemplo,

lemma "longitud (repite n x) = n"

También se puede poner un nombre al lema, por ejemplo,

lemma inversaAcAux_es_inversa:
  "inversaAcAux xs ys = (inversa xs)@ys"

La demostración es la palabra by seguida por el método de demostración. Los métodos que hemos usado son

  • by simp: que es el método de simplificación por reescritura,
  • by (induct x) auto: que es por inducción en x (donde x es un número natural o una lista) y simplificación automática de ambos casos,
  • by (induct rule: fn.induct) auto: que es por inducción según la definición de la función fn y simplificación automática de todos los casos,
  • by (simp add: lema_auxiliar): que es el método de simplificación por reescritura añadiéndole a las reglas de reescritura la correspondiente al lema_auxiliar,

La teoría con los ejemplos presentados en la clase es la siguiente:

Reseña: “Concrete semantics” with Coq and CoqHammer

Se ha publicado un artículo de razonamiento formalizado en Coq titulado “Concrete semantics” with Coq and CoqHammer.

Sus autores son

Su resumen es

The “Concrete Semantics” book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of the book using the Coq proof assistant. In order to achieve a similar brevity of the formal text we extensively use CoqHammer, as well as Coq Ltac-level automation. We compare the formalization efficiency, compactness, and the readability of the proof scripts originating from a Coq re-formalization of two chapters from the book.

El trabajo se ha presentado el 15 de agosto en el CICM 2018 (11th Conference on Intelligent Computer Mathematics).

El código de las correspondientes teorías se encuentra en GitHub.

Reseña: Comparison of two theorem provers: Isabelle/HOL and Coq

Se ha publicado un artículo de demostración asistida por ordenador titulado Comparison of two theorem provers: Isabelle/HOL and Coq.

Sus autores son

Su resumen es

The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the danger of accumulating errors across theories. Although, according to Gödel’s incompleteness theorems, it is not possible to construct a single formal system which will describe all phenomena in the world, being complete and consistent at the same time, it gave rise to rather practical areas of logic, such as the theory of automated theorem proving. This is a set of techniques used to verify mathematical statements mechanically using logical reasoning. Moreover, it can be used to solve complex engineering problems as well, for instance, to prove the security properties of a software system or an algorithm. This paper compares two widespread tools for automated theorem proving, Isabelle/HOL and Coq, with respect to expressiveness, limitations and usability. For this reason, it firstly gives a brief introduction to the bases of formal systems and automated deduction theory, their main problems and challenges, and then provides detailed comparison of most notable features of the selected theorem provers with support of illustrative proof examples.

Reseña: A formal proof of the computation of Hermite normal form in a general setting

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado REGULAR-MT: A formal proof of the computation of Hermite normal form in a general setting.

Sus autores son Jose Divasón y Jesús Aransay (de la Universidad de la Rioja).

Su resumen es

In this work, we present a formal proof of an algorithm to compute the Hermite normal form of a matrix based on our existing framework for the formalisation, execution, and refinement of linear algebra algorithms in Isabelle/HOL. The Hermite normal form is a well-known canonical matrix analogue of reduced echelon form of matrices over fields, but involving matrices over more general rings, such as Bézout domains. We prove the correctness of this algorithm and formalise the uniqueness of the Hermite normal form of a matrix. The succinctness and clarity of the formalisation validate the usability of the framework.

El trabajo se presentará el 17 de septiembre en el AISC 2018 (13th International Conference on Artificial Intelligence and Symbolic Computation).

El código de las correspondientes teorías se encuentra aquí.

LMF2017: Ejercicios de lógica de primer orden

En la clase de hoy del curso Lógica matemática y fundamentos se han comentado soluciones de ejercicios de lógica de primer orden. Concretamente,

LMF2017: Deducción natural de primer orden con Isabelle/HOL

En la clase de hoy del curso de Lógica matemática y fundamentos se ha presentado la deducción natural de primer orden Isabelle/HOL. La presentación se basa en los ejemplos del tema 8 que, a su vez, se basa en el capítulo 2 del libro de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).

La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración.

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, las siguientes van eliminando detalles de la prueba hasta la última que es automática.

A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.

La teoría con los ejemplos presentados en la clase es la siguiente: