Introduzione di O-grande in Isabelle

The thesis presents the formalization of the BigO asymptotic notation in Isabelle, proposed by J.Avigad and K. Donnelly. The paper is divided into 3 chapters which deal respectively with: 1. Introduction of the topic through the basic concepts 2. Formalization of the concepts used in Isabelle 3. Demonstration of the correctness of the formalization and its properties The sources used for the drafting allow to deepen the essential points reported in the original work by J.Avigad and K. Donnelly. The conclusion shows the future implications of this theory, also proposing a possible improvement.

La tesi presenta la formalizzazione della notazione asintotica BigO in Isabelle, proposta da J.Avigad e K.Donnelly. L'elaborato si articola in 3 capitoli che trattano rispettivamente di: 1. Introduzione dell'argomento mediante i concetti di base 2. Formalizzazione in Isabelle dei concetti utilizzati 3. Dimostrazione della correttezza della formalizzazione e delle sue proprietà Le fonti utilizzate per la stesura permettono di approfondire i punti essenziali riportati nel lavoro originale di J.Avigad e K.Donnelly. Nella conclusione vengono mostrati i risvolti futuri di questa teoria proponendo anche un possibile miglioramento.