– PSI

Les assistants à la preuve fournissent un formalisme logique très expressif, de fait suffisamment riche pour permettre une description extrêmement précise d'objets complexes comme la meta-théory d'un langage de programmation (Harper07), un modèle de compilateur C (Leroy-compcert-06), ou la preuve du théorème des Quatre Couleurs (Gonthier08). Cette description inclut aussi bien les énoncés logiques de propriétés requises pour les objets mais aussi leur preuve formelle. Ces preuves sont impitoyablement vérifiées par le vérificateur de preuves du système, qui doit être un programme de petite taille, auquel on peut donc faire confiance. Par exemple, dans le cas de la spécification de la correction d'un programme, ces systèmes fournissent la plus élevée des garanties formelles possibles. La recherche de preuves est un problème central dans une telle approche de la formalisation des mathématiques. Il s'agit aussi d'un axe commun au raisonnement automatique et à des paradigmes haut niveau comme la Programmation Logique. Il est alors tentant de concevoir un cadre logique dans lequel une notion générique de recherche de preuve puisse sous-tendre chacun des points de vues évoqués précédemment. Néanmoins, en pratique les application de ces techniques incluent des logiques et des théories spécifique, typiquement l'arithmétique linéaire. Qu'un tel cadre logique générique puisse ou non exprimer ces spécificités, il est hautement improbable que des méthodes de recherche de preuves génériques puissent remplacer des outils spécifiques à une logique ou une théorie. En effet, la théorie spécifique peut être en dehors du cadre que la recherche de preuve générique sait prendre en compte. Mais plus sûrement, une méthode de recherche de preuves générique sera moins efficace qu'une procédure ad-hoc, typiquement une procédure de décision. Mais pour étendre la portée des méthodes de décision spécifiques, on peut les combiner avec des mécanismes génériques de recherche de preuves. C'est une approche similaire qui est adoptée dans les architectures de Satisfiabilité Modulo Théories (SMT) (SMT) (Nieuwenhuisetal2006JACM) et Programmation Logique par Contraintes (CLP(X)) (JaffarM94): exploiter une décision efficace sur une théorie spécifique, au sein d'un outil générique. Dans le cas de CLP(X), l'outil générique est un noyau de programmation logique, alors que dans le cas SMT, il s'agit d'un SAT solver. Cette ingénieuse extension des SAT solvers a ouvert une aire de recherche prolifique, et rapidement devenue cruciale pour de nombreuses application en vérification (JinHS05,LernerMC03,VelevB03). Dans l'architecture SMT, un processus central organise le dialogue entre deux composants : il fournit au SAT solver la structure purement logique du problème, ignorant les atomes de la formule, puis récupère (si possible) une proposition de modèle de satisfiabilité, et enfin vérifie grâce à l'outil spécifique la consistence du modèle par rapport à la théorie. L'idée est donc de demander un certain niveau d'interaction entre les deux niveaux d'automatisation, ne serait-ce que pour réduire un problème dans le domaine traité par une méthode spécifique à une théorie. Une telle réduction peut être très simple et apparaître comme une sorte de pre-processing. Mais même dans ce cas, il est intéressent d'implémenter un tel pre-processing ainsi que l'appel à une méthode spécifique dans un schéma modulaire. Néanmoins cette réduction peut aussi être non triviale (ex. logique du premier ordre) et nécessiter un travail substantiel de la part des outils de recherche de preuves. De fait, si ces quinze dernières années, de nouvelles fonctionnalités (polarisation, focusing,etc.) ont émergé pour améliorer les mécanismes de recherche de preuves au coeur de la programmation logique, ces fonctionnalités ont été pensées pour être des stratégies complétant totalement les preuves. Mais dans ce contexte, nous voulons être guidés par un objectif plus général, atteindre un point ou une méthode spécifique supposée disponible peut être appliquée. Notre point de départ est ainsi de considérer à la fois la théorie de la démonstration et le paradigme de la programmation logique pour expérimenter jusqu'à quel point on peut étendre l'architecture SMT en direction de logiques plus expressives, se donnant de ce fait du contrôle sur le processus de recherche de preuves.