Integrating rewriting, tableau and superposition into SMT
Guillaume Bury · 2019
Intégrer la réecriture, la méthode des tableaux et la superposition dans les solveurs SMT Cette thèse doctorale présente ArchSAT, un théorème prouveur capable de générer des preuves formelles, qui est utilisé pour étudier l’intégration à l’algorithme SMT de techniques de raisonnements dits "du premier ordre". ArchSAT intègre la réecriture grâce à une théorie SMT standard,qui permet d’accélérer la vitesse du raisonnement sur les problèmes dont certains axiomes peu-vent être vus comme des règles de réécriture. De plus, une extension de cette théorie adaptée à l’algorithme McSAT (plutôt que SMT), permet aussi de gérer les règles de réécriture conditionnelles. ArchSAT intègres aussi la méthode des tableaux au travers d’une théorie SMT traditionnelle, afin de raisonner de manière générique sur tout le premier ordre, ce qui permet de remplacer la transformation en forme normal conjonctive et le mécanisme des triggers habituellement utilisés dans les prouveurs SMT. Cette théorie SMT pour la méthode des tableaux utilise par ailleurs une variante de la superposition afin d’unifier des termes modulo égalités et règles de réécriture.Finalement, ArchSAT est capable de générer des preuves formelles à la fois pour l’assistant de preuve Coq, et le framework logique dedukti, ce qui permet d’assurer la correction des résultats.