Automatic demonstration of mathematical conjectures
Magera, Floriane
Promoteur(s) : Boigelot, Bernard
Date de soutenance : 8-sep-2016/9-sep-2016 • URL permanente : http://hdl.handle.net/2268.2/1679
Détails
Titre : | Automatic demonstration of mathematical conjectures |
Titre traduit : | [fr] Démonstration automatique de conjectures mathématiques |
Auteur : | Magera, Floriane |
Date de soutenance : | 8-sep-2016/9-sep-2016 |
Promoteur(s) : | Boigelot, Bernard |
Membre(s) du jury : | Gribomont, Pascal
Wolper, Pierre Rigo, Michel |
Langue : | Anglais |
Nombre de pages : | 80 |
Discipline(s) : | Ingénierie, informatique & technologie > Sciences informatiques |
Public cible : | Grand public |
URL complémentaire : | https://github.com/flomage2612/TFE |
Institution(s) : | Université de Liège, Liège, Belgique |
Diplôme : | Master en ingénieur civil en informatique, à finalité approfondie |
Faculté : | Mémoires de la Faculté des Sciences appliquées |
Résumé
[en] A particular logic has been introduced for reasoning about automatic sequences. An automatic sequence is roughly speaking an infinite word that can be generated by a deterministic finite automaton. Properties of these sequences defined with quantifiers, logical operators, integer variables, addition, indexing on the sequence, and comparison operators are decidable.
This work is focusing on a tool, Walnut, developed for automating decision procedures for this logic.
This tool allows to use natural numbers encoded in various numeration systems (binary, decimal, hexadecimal numeration systems are common in computer science). One interesting feature of the tool is the allowance to add new numeration systems if the addition automaton for this numeration system is provided. The user must thus provide an automaton accepting the language L = {(x,y,z)} with (x,y,z) being the encoding of three natural numbers in the numeration system, and such that the values represented by x and y added together give the value represented by z.
The aim of this master thesis is to automate the generation of the addition automaton for the Fibonacci numeration systems. An original solution has been developed for this problem using automata. This new method is inspired from existing work, ensuring some interesting efficiency properties. A working implementation has been provided in order to generate the addition automaton in a dot file.
Fichier(s)
Document(s)
Description:
Taille: 1.18 MB
Format: Adobe PDF
Citer ce mémoire
L'Université de Liège ne garantit pas la qualité scientifique de ces travaux d'étudiants ni l'exactitude de l'ensemble des informations qu'ils contiennent.