Faculté des Sciences appliquées
Faculté des Sciences appliquées

Automatic demonstration of mathematical conjectures

Magera, Floriane ULiège
Promotor(s) : Boigelot, Bernard ULiège
Date of defense : 8-Sep-2016/9-Sep-2016 • Permalink :
Title : Automatic demonstration of mathematical conjectures
Translated title : [fr] Démonstration automatique de conjectures mathématiques
Author : Magera, Floriane ULiège
Date of defense  : 8-Sep-2016/9-Sep-2016
Advisor(s) : Boigelot, Bernard ULiège
Committee's member(s) : Gribomont, Pascal ULiège
Wolper, Pierre ULiège
Rigo, Michel ULiège
Language : English
Number of pages : 80
Discipline(s) : Engineering, computing & technology > Computer science
Target public : General public
Complementary URL :
Institution(s) : Université de Liège, Liège, Belgique
Degree: Master en ingénieur civil en informatique, à finalité approfondie
Faculty: Master thesis of the Faculté des Sciences appliquées


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



Access Automatic_demonstration_of_mathematical_conjectures.pdf
Size: 1.18 MB
Format: Adobe PDF


  • Magera, Floriane ULiège Université de Liège > Master ingé. civ. info., fin. appr. (ex 2e master)


Committee's member(s)

  • Gribomont, Pascal ULiège Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique et intelligence artificielle
    ORBi View his publications on ORBi
  • Wolper, Pierre ULiège Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données)
    ORBi View his publications on ORBi
  • Rigo, Michel ULiège Université de Liège - ULg > Département de mathématique > Mathématiques discrètes
    ORBi View his publications on ORBi
  • Total number of views 486
  • Total number of downloads 321

All documents available on MatheO are protected by copyright and subject to the usual rules for fair use.
The University of Liège does not guarantee the scientific quality of these students' works or the accuracy of all the information they contain.