Reseña: Proving divide and conquer complexities in Isabelle/HOL
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.