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.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.