En la clase de hoy del curso de Razonamiento automático se ha presentado la programación funcional en Isabelle/HOL.
La teoría con los ejemplos presentados en la clase es la siguiente:
Como tarea se propuso la resolución de los ejercicios de la 1ª relación.
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Proving divide and conquer complexities in Isabelle/HOL
Su autor es Manuel Eberl (de la Technische Universität München, Alemania).
Su resumen es
The Akra–Bazzi method, a generalisation of the well-known Master Theorem, is a useful tool for analysing the complexity of Divide & Conquer algorithms. This work describes a formalisation of the Akra–Bazzi method (as generalised by Leighton) in the interactive theorem prover Isabelle/HOL and the derivation of a generalised version of the Master Theorem from it. We also provide some automated proof methods that facilitate the application of this Master Theorem and allow mostly automatic verification of Θ-bounds for these Divide & Conquer recurrences. To our knowledge, this is the first formalisation of theorems for the analysis of such recurrences.
La versión final del trabajo se ha publicado en el Journal of Automated Reasoning.
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.
Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre álgebra titulado A decision procedure for univariate real polynomials in Isabelle/HOL.
Su autor es Manuel Eberl (de la Technische Universität München, Alemania).
Su resumen es
Sturm sequences are a method for computing the number of real roots of a univariate real polynomial inside a given interval efficiently. In this paper, this fact and a number of methods to construct Sturm sequences efficiently have been formalised with the interactive theorem prover Isabelle/HOL. Building upon this, an Isabelle/HOL proof method was then implemented to prove interesting statements about the number of real roots of a univariate real polynomial and related properties such as non-negativity and monotonicity.
El trabajo se ha presentado en la CPP 2015 (The 4th ACM-SIGPLAN Conference on Certified Programs and Proofs).
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Relation-algebraic verification of Prim’s minimum spanning tree algorithm.
Su autor es Walter Guttmann (de la University of Canterbury, Nueva Zelanda).
Su resumen es
We formally prove the correctness of Prim’s algorithm for computing minimum spanning trees. We introduce new generalisations of relation algebras and Kleene algebras, in which most of the proof can be carried out. Only a small part needs additional operations, for which we introduce a new algebraic structure. We instantiate these algebras by matrices over extended reals, which model the weighted graphs used in the algorithm. Many existing results from relation algebras and Kleene algebras generalise from the relation model to the weighted-graph model with no or small changes. The overall structure of the proof uses Hoare logic. All results are formally verified in Isabelle/HOL heavily using its integrated automated theorem provers.
El trabajo se presentará el 24 de octubre en el ICTAC2016 (13th International Colloquium on Theoretical Aspects of Computing).
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado A framework for verifying depth-first search algorithms in Isabelle/HOL.
Sus autores son Peter Lammich y René Neumann (de la Technische Universität München)
Su resumen es
Many graph algorithms are based on depth-first search (DFS).The formalizations of such algorithms typically share many common ideas. In this paper, we summarize these ideas into a framework in Isabelle/HOL.
Building on the Isabelle Refinement Framework, we provide support for a refinement based development of DFS based algorithms, from phrasing and proving correct the abstract algorithm, over choosing an adequate implementation style (e. g., recursive, tail-recursive), to creating an executable algorithm that uses efficient data structures.
As a case study, we verify DFS based algorithms of different complexity, from a simple cyclicity checker, over a safety property model checker, to complex algorithms like nested DFS and Tarjan’s SCC algorithm.
El trabajo se ha presentado en The 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015)
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.