Reseña: Landau symbols en Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Landau symbols en Isabelle/HOL.

Sus autor es Manuel Eberl (del Theorem Proving Group en la Technische Universität München, Munich, Alemania).

Su resumen es

This entry provides Landau symbols to describe and reason about the asymptotic growth of functions for sufficiently large inputs. A number of simplification procedures are provided for additional convenience: cancelling of dominated terms in sums under a Landau symbol, cancelling of common factors in products, and a decision procedure for Landau expressions containing products of powers of functions like x, ln(x), ln(ln(x)) etc.

El trabajo se ha publicado en The Archive of Formal Proofs.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

Este trabajo puede servir como lectura complementaria del curso de Razonamiento automático.