Reseña: The Akra-Bazzi theorem and the Master theorem
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado The Akra-Bazzi theorem and the Master theorem.
Su autor es Manuel Eberl (del Theorem Proving Group en la Technische Universität München, Munich, Alemania).
Su resumen es
This article contains a formalisation of the Akra-Bazzi method based on a proof by Leighton. It is a generalisation of the well-known Master Theorem for analysing the complexity of Divide & Conquer algorithms. We also include a generalised version of the Master theorem based on the Akra-Bazzi theorem, which is easier to apply than the Akra-Bazzi theorem itself.
Some proof methods that facilitate applying the Master theorem are also included. For a more detailed explanation of the formalisation and the proof methods, see the accompanying paper (publication forthcoming).
El trabajo se ha publicado en AFP (The Archive of Formal 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 y Lógica computacional y teoría de modelos.