The subject of the thesis concerns the study of infinite sequences, in one or two dimensions, supporting the theoretical aspects with systems for symbolic and logic computation. In particular, in the thesis some sequences related to Riordan arrays are examined from both an algebraic and combinatorial points of view and also by using approaches usually applied in numerical analysis. Another part concerns sequences that enumerate particular combinatorial objects, such as trees, polyominoes, and lattice paths, generated by symbolic and certified computations; moreover, tiling problems and backtracking techniques are studied in depth and enumeration of recursive structures are also given. We propose a preliminary suite of tools to interact with the Online Encyclopedia of Integer Sequences, providing a crawling facility to download sequences recursively according to their cross references, pretty-printing them and, finally, drawing graphs representing their connections. In the context of automatic proof derivation, an extension to an automatic theorem prover is proposed to support the relational programming paradigm. This allows us to encode facts about combinatorial objects and to enumerate the corresponding languages by producing certified theorems at the same time. As a concrete illustration, we provide many chunks of code written using functional programming languages; our focus is to support theoretical derivations using sound, clear and elegant implementations to check their validity.

An algebraic and combinatorial study of some infinite sequences of numbers supported by symbolic and logic computation / MASSIMO NOCENTINI. - (2019).

An algebraic and combinatorial study of some infinite sequences of numbers supported by symbolic and logic computation.

MASSIMO NOCENTINI
2019

Abstract

The subject of the thesis concerns the study of infinite sequences, in one or two dimensions, supporting the theoretical aspects with systems for symbolic and logic computation. In particular, in the thesis some sequences related to Riordan arrays are examined from both an algebraic and combinatorial points of view and also by using approaches usually applied in numerical analysis. Another part concerns sequences that enumerate particular combinatorial objects, such as trees, polyominoes, and lattice paths, generated by symbolic and certified computations; moreover, tiling problems and backtracking techniques are studied in depth and enumeration of recursive structures are also given. We propose a preliminary suite of tools to interact with the Online Encyclopedia of Integer Sequences, providing a crawling facility to download sequences recursively according to their cross references, pretty-printing them and, finally, drawing graphs representing their connections. In the context of automatic proof derivation, an extension to an automatic theorem prover is proposed to support the relational programming paradigm. This allows us to encode facts about combinatorial objects and to enumerate the corresponding languages by producing certified theorems at the same time. As a concrete illustration, we provide many chunks of code written using functional programming languages; our focus is to support theoretical derivations using sound, clear and elegant implementations to check their validity.
2019
Donatella Merlini
ITALIA
Goal 4: Quality education
MASSIMO NOCENTINI
File in questo prodotto:
File Dimensione Formato  
PhD-thesis Nocentini Massimo.pdf

accesso aperto

Tipologia: Tesi di dottorato
Licenza: Open Access
Dimensione 3.65 MB
Formato Adobe PDF
3.65 MB Adobe PDF

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/1217082
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact