Stronger SMT Solvers for Proof Assistants : Proofs, Quantifier Simplification, Strategy Schedules

Consolidation des solveurs SMT pour les assistants de preuve : preuves, simplification des quantificateurs, planification de stratégies Cette thèse présente trois contributions qui ont pour objectif d'améliorer l'utilité des solveurs SMT comme backends pour les assistants de preuve. Les solveurs SMT sont des outils de démonstration automatique de théorèmes qui intègrent le raisonnement propositionnel avec des théories. Un assistant de preuve est un logiciel qui permet aux utilisateurs d'écrire des preuves vérifiées formellement. Pour aider l'utilisateur, les assistants de preuve proposent certaines automatisations utilisant des outils de démonstration automatiques. Les assistants de preuve n'acceptent généralement que les preuves qui utilisent le formalisme proposé par l'assistant. La première contribution traite de la reconstruction de preuves SMT dans un assistant de preuve. Nous présentons le format de preuve Alethe pour les solveurs SMT. Il améliore et unifie les travaux antérieurs sur la génération de preuves à partir de solveurs SMT. La grande majorité de ces améliorations a été inspirée par l'expérience acquise par un travail substantiel visant à la reconstruction de preuves Alethe dans l'assistant de preuve Isabelle/HOL. Les problèmes SMT générés par les assistants de preuve dépendent largement des quantificateurs. Puisque les solveurs SMT sont particulièrement adaptés aux problèmes sans quantificateurs, ils utilisent l'instantation des quantificateurs pour générer des formules sans quantificateurs. La deuxième contribution améliore l'instanciation des quantificateurs. Il s'agit d'une méthode basée sur l'unification qui enrichie le problème avec des formules quantifiées superficielles obtenues à partir d'assertions avec des quantificateurs imbriqués. Ces nouvelles formules aident à débloquer l'utilisation des techniques d'instanciation classiques, mais elles doivent être utilisées avec parcimonie car elles peuvent aussi être mal interprétées. Cette méthode permet au solveur de prouver plus de formules, plus rapidement. L'utilisation d'un solveur SMT est fortement paramétrable. Un paramétrage spécifique est appelé une stratégie, et la meilleure stratégie diffère généralement d'un problème à l'autre. La troisième contribution est une panoplie d'outils destinée à faciliter l'utilisation et le choix de ces stratégies. Un des outils majeurs propose d'utiliser l'optimisation linéaire en nombres entiers pour générer des planificateurs de stratégie. La panoplie d'outils proposée contient également des outils de simulation et d'analyse des planifications. Cet ensemble d'outils est utilisé pour determiner les stratégies permettant de résoudre certains problèmes générés par Isabelle/HOL.