Haniel Barbosa

Erika Ábrahám

David Déharbe

Catherine Dubois

Pascal Fontaine

Stephan Merz

Jordi Martori

Jonàs Martínez

Aybüke Özgün

Maike Massierer

Martin Riener

Simon Cruanes

Keywords: quantifier instantiation, proof production, proof automation, smt solving, formal verification

In many formal methods applications it is common to rely on SMT solvers to automatically discharge conditions that need to be checked and provide certificates of their results. In this thesis we aim both to improve their efficiency of and to increase their reliability.

Our first contribution is a uniform framework for reasoning with quantified formulas in SMT solvers, in which generally various instantiation techniques are employed. We show that the major instantiation techniques can be all cast in this unifying framework. Its basis is the problem of E-ground (dis)unification, a variation of the classic rigid E -unification problem. We introduce a decision procedure to solve this problem in practice: Congruence Closure with Free Variables (CCFV). We measure the impact of optimizations and instantiation techniques based on CCFV in the SMT solvers veriT and CVC4, showing that our implementations exhibit improvements over state-of-the-art approaches in several benchmark libraries stemming from real world applications.

Our second contribution is a framework for processing formulas while producing detailed proofs. The main components of our proof producing framework are a generic contextual recursion algorithm and an extensible set of inference rules. With suitable data structures, proof generation creates only a linear-time overhead, and proofs can be checked in linear time. We also implemented the approach in veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced.

Résumé

Des nombreuses applications de méthodes formelles se fonde sur les solveurs SMT pour valider automatiquement les conditions à vérifier et fournissent des certificats de leurs résultats. Dans cette thèse, nous visons à la fois à améliorer l'efficacité des solveurs SMT et à accroître leur fiabilité.

Notre première contribution est un cadre uniforme pour le raisonnement avec des formules quantifiées dans les solveurs SMT, dans lequel généralement diverses techniques d'instanciation sont utilisées. Nous montrons que les principales techniques d'instanciation peuvent être jetées dans ce cadre. Le cadre repose sur le problème de l'E-ground (dis)unification. Nous présentons un procédure de décision pour résoudre ce problème en pratique: Fermeture de congruence avec variables libres (CCFV). Nous mesurons l'impact des CCFV dans les solveurs SMT veriT et CVC4. Nous montrons que nos implémentations présentent des améliorations par rapport aux approches à la fine pointe de la technologie dans plusieurs bibliothèques de référence issues d'applications du monde réel.

Notre deuxième contribution est un cadre pour le traitement des formules tout en produisant des preuves détaillées. Les principaux composants de notre cadre de production de preuve sont un algorithme de récurrence contextuelle générique et un ensemble extensible de règles d'inférence. Avec des structures de données appropriées, la génération des preuves ne crée que des frais généraux linéaires et les vérifications peuvent être vérifiées en temps linéaire. Nous avons également mis en oeuvre l'approche en veriT. Cela nous a permis de simplifier considérablement la base du code tout en augmentant le nombre de problèmes pour lesquels des preuves détaillées peuvent être produites.

Mots-clés: instanciation des quantificateurs, production des démonstrations, automatisation des démonstrations, résolution smt, vérification formelle.

Resumo

Em muitas aplicações de métodos formais, como verificação formal, síntese de programas, testes automáticos e análise de programas, é comum depender de solucionadores de satisfatibilidade módulo teorias (SMT) como backends para resolver automaticamente condições que precisam ser verificadas e fornecer certificados de seus resultados. Nesta tese, objetivamos melhorar a eficiência dos solucionadores SMT e aumentar sua confiabilidade.

Nossa primeira contribuição é fornecer um arcabouço uniforme e eficiente para raciocinar com fórmulas quantificadas em solucionadores SMT, em que, geralmente, várias técnicas de instanciação são empregadas para lidar com quantificadores. Mostramos que as principais técnicas de instanciação podem ser lançadas neste arcabouço unificador para lidar com fórmulas quantificadas com igualdade e funções não interpretadas. O arcabouço baseia-se no problema de E -ground (dis)unificação, uma variação do problema clássico de E -unificação rígida. Apresentamos um cálculo correto e completo para resolver esse problema na prática: Fechamento de Congruência com Variáveis Livres (CCFV). Uma avaliação experimental é apresentada, na qual medimos o impacto das otimizações e técnicas de instanciação baseadas no CCFV nos solucionadores SMT veriT e CVC4. Mostramos que nossas implementações exibem melhorias em relação às abordagens de última geração em várias bibliotecas de referência, decorrentes de aplicações do mundo real.

Nossa segunda contribuição é uma estrutura para o processamento de fórmulas ao mesmo tempo que produz demonstrações detalhadas. Nosso objetivo é aumentar a confiabilidade nos resultados de solucionadores SMT e sistemas de raciocínio automatizado similares, fornecendo justificativas que podem ser verificadas com eficiência de forma independente e para melhorar sua usabilidade por aplicativos externos. Os assistentes de demonstração, por exemplo, geralmente requerem a reconstrução da justificação fornecida pelo solucionador em uma determinada obrigação de prova.

Os principais componentes da nossa estrutura de produção de demonstrações são um algoritmo genérico de recursão contextual e um conjunto extensível de regras de inferência. Clausificação, Skolemização, simplificações específicas de teorias e expansão das expressões "let" são exemplos dessa estrutura. Com estruturas de dados adequadas, a geração de demonstrações cria apenas uma sobrecarga de tempo linear, e as demonstrações podem ser verificadas em tempo linear. Também implementamos a abordagem em veriT. Isso nos permitiu simplificar drasticamente a base do código, aumentando o número de problemas para os quais demonstrações detalhadas podem ser produzidas.

Palavras-chave: instanciação de quantificadores, produção de demonstrações, automatizaçao de demonstrações, resulução smt, verificação formal.

Extended Abstract in French

Introduction Dans de nombreuses applications des méthodes formelles, telles que la vérification formelle, la synthèse de programmes, les tests automatiques et l'analyse de programme, il est fréquent de s'appuyer sur la logique pour représenter des conditions de vérification qui doivent être validées.

Ces conditions peuvent souvent être réduites au problème de la satisfiabilité modulo des théories (SMT) (Chapitre 2): étant donné une formule logique de premier ordre, y a-t-il un modèle compatible avec une combinaison de théories d'arrière-plan? Les solveurs SMT sont ainsi devenus des backends populaires pour les outils d'automatisation de la vérification formelle, la synthèse de programmes, etc. . . Ils valident automatiquement les obligations de preuve -conditions à vérifier -et fournissent des certificats de leurs résultats, c'est-à-dire des modèles ou des preuves. Dans cette thèse, nous visons à la fois à améliorer l'efficacité des solveurs SMT et à accroître leur fiabilité.

Les solveurs SMT (Chapitre 3) ont été initialement conçus pour résoudre des problèmes sans quantification, sur lesquels ils sont très efficaces et capables de traiter de grandes formules avec des symboles interprétés. La logique du premier ordre pure avec quantificateurs est traitée plus avantageusement avec la résolution et la superposition [START_REF] Bachmair | Rewrite-Based Equational Theorem Proving with Selection and Simplification[END_REF][START_REF] Nieuwenhuis | Paramodulation-Based Theorem Proving[END_REF]. Bien qu'il existe des premières tentatives [START_REF] De | Engineering DPLL(T) + Saturation[END_REF] pour unifier ces techniques avec CDCL(T ) [START_REF] Nieuwenhuis | Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)[END_REF] (le calcul que les solveurs SMT implémentent habituellement), l'approche la plus commune est encore l'instanciation: les formules quantifiées sont réduites à des formules sans quantificateurs ellesmême réfutées avec l'aide de procédures de décision pour les formules sans quantificateurs. Les principales techniques d'instanciation sont le E -matching basé sur les tiggers [START_REF] Detlefs | Simplify: A Theorem Prover for Program Checking[END_REF][START_REF] De | Efficient E-Matching for SMT Solvers[END_REF][START_REF] Rümmer | E-Matching with Free Variables[END_REF], la recherche d'instances conflictuelles [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF] et l'instanciation de quantificateurs basée sur les modèles (MBQI) [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF][START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF]. Chacune de ces techniques contribue à l'efficacité des solveurs modernes, mais chacune est généralement implémentée indépendamment.

Nous présentons le problème de E-ground (dis)unification comme la pierre angulaire d'un cadre unique dans lequel toutes ces techniques peuvent être exprimées (Chapitre 4). Ce problème est lié au problème classique de E -unification [START_REF] Degtyarev | What You Always Wanted to Know about Rigid E-Unification[END_REF] rigide et est également NP-complet.

Résoudre le problème de E-ground (dis)unification se ramène à la recherche de substitutions telles que les littéraux contenant des variables libres soient substitués en littéraux présents dans le problème sans quantificateurs. Étant donné que le domaine d'instanciation de ces variables xiv est borné, un moyen possible de résoudre le problème est d'abord de déterminer de façon non déterministe une substitution et de vérifier s'il s'agit d'une solution. L'algorithme de Fermeture de congruence avec variables libres (congruence closure with free variables, CCFV) présenté ici est une procédure de décision pratique pour ce problème qui s'appuie sur l'algorithme classique de fermeture de congruence [START_REF] Nelson | Fast Decision Procedures Based on Congruence Closure[END_REF][START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF]. Il est axé sur les objectifs: les solutions sont construites de manière incrémentielle, compte tenu de la fermeture de congruence des termes définis par les égalités dans le contexte et des attributions possibles aux variables. Nous montrons ensuite comment se baser sur CCFV pour implémenter une instanciation basée sur les triggers, sur les conflits ou sur les modèles (Chapitre 5). Une évaluation expérimentale est présentée, dans laquelle nous mesurons l'impact des optimisations et des techniques d'instanciation basées sur CCFV.

Nous montrons que nos implémentations présentent des améliorations par rapport à l'état de l'art. Il s'agit d'un travail en commun avec Pascal Fontaine et Andrew Reynolds [START_REF] Barbosa | Congruence Closure with Free Variables[END_REF].

Les techniques d'instanciation pour SMT ont été largement étudiées. L'instanciation heuristique basée sur E -matching des déclencheurs sélectionnés a d'abord été introduite par Nelson [START_REF] Gregory | Techniques for Program Verification[END_REF] et a été mise en oeuvre avec succès dans plusieurs solveurs. Une implémentation très efficace de E -matching dans le contexte des solveurs SMT a été présentée par de Moura et Bjørner [START_REF] De | Efficient E-Matching for SMT Solvers[END_REF]; Elle s'appuie sur des algorithmes d'unification incrémentaux, une génération de code machine pour optimiser les performances et des techniques d'indexation élaborées ayant des caractéristiques communes avec les indexages pour les testeurs de théorèmes basés sur la saturation. Rümmer utilise des trigger avec d'une méthode classique de tableaux [START_REF] Rümmer | E-Matching with Free Variables[END_REF].

L'instanciation basée sur les triggers produit malheureusement de nombreuses instances non pertinentes. Pour aborder ce problème, une technique d'instanciation axée sur les objectifs produisant uniquement des instances utiles a été introduite par Reynolds et al. [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF]. CCFV partage des similarités avec cet algorithme, la recherche étant basée sur la structure des termes et un modèle actuel provenant du solveur pour la partie sans quantificateurs. L'approche ici est cependant plus générale, la technique précédente étant une spécialisation. L'instanciation de quantificateurs basée sur les modèles de Ge and de Moura (MBQI) [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF] fournit une méthode complète pour la logique du premier ordre grâce à la dérivation successive d'instances conflictuelles afin d'affiner un modèle candidat pour l'ensemble de la formule, quantificateurs compris. Des méthodes alternatives pour la construction et la vérification des modèles ont été présentées par Reynolds et al. [START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF]. Ces deux approches basées sur le modèle [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF][START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF] permettent l'intégration des théories au-delà de l'égalité, tandis que CCFV ne gère pour l'instant que l'égalité et les fonctions non interprétées. Backeman et Rümmer résolvent le problème connexe de l'E -unification rigide à travers le codage dans SAT, en utilisant un solveur SAT off-the-shelf pour calculer des solutions [START_REF] Backeman | Theorem Proving with Bounded Rigid E-Unification[END_REF]. Notre travail est plus dans la lignée des techniques telles que celles de Goubault [START_REF] Goubault | A rule-based algorithm for rigid E-unification[END_REF] et Tiwari et al. [START_REF] Tiwari | Rigid E-Unification Revisited[END_REF], les algorithmes de fermeture de congruence étant très efficaces pour vérifier les solutions, nous pensons qu'ils peuvent aussi constituer le noyau d'algorithmes efficaces pour les découvrir. CCFV diffère de ces techniques antérieures notamment, car elle gère les inégalités et que la recherche de solutions xv Extended Abstract in French est guidée par la structure d'un modèle pour la formule sans quantificateurs et est donc la plus appropriée pour un contexte SMT.

Un aspect très important dans le raisonnement automatisé est de fournir des certificats vérifiables par machine pour les résultats produits. Les applications externes utilisant des systèmes automatiques ne nécessitent généralement pas seulement la réponse au problème de satisfaction, mais aussi une justification. Par exemple, en vérifiant si un théorème est valide en essayant de montrer que sa négation est insatisfaisante, produire un modèle dans le cas d'une formule satisfaisable fournit un contre-exemple pour la conjecture. En outre, étant donné que ces systèmes peuvent être des logiciels complexes, souvent avec des centaines de milliers de lignes de code, il est difficile de s'assurer que les implémentations sont exemptes d'erreurs. Par conséquent, être en mesure de vérifier les résultats obtenus est d'une importance primordiale pour améliorer la fiabilité d'un tel outil.

Un nombre croissant de prouveurs de théorèmes automatiques peuvent générer des certificats, ou des preuves, qui justifient leurs résultats. Ces preuves peuvent être vérifiées par d'autres programmes et partagées entre les systèmes de raisonnement. La production de preuve est généralement bien comprise pour les méthodes de preuve de base (par exemple, la superposition, les tableaux, l'apprentissage de clauses axé sur les conflits) et pour de nombreuses théories couramment utilisées en SMT. Cependant, la plupart des prouveurs automatiques effectuent également un traitement ou un prétraitement de formule -comme la clausification et la réécriture avec des lemmes spécifiques à la théorie -et la production de preuve pour cet aspect est moins bien comprise. Pour la plupart des prouveurs, le code pour préprocesser les formules n'est pas particulièrement compliqué, mais il est long et traite une multitude de cas, dont certains sont rarement exécutés. Bien qu'il soit crucial pour l'efficacité, ce code tend à recevoir beaucoup moins d'attention que d'autres aspects des prouveurs. Les développeurs sont réticents à investir de l'effort en produisant des preuves détaillées pour un tel traitement, car cela nécessite d'adapter beaucoup de code. En conséquence, la granularité des inférences pour le traitement de la formule est souvent grossière. Parfois, les fonctionnalités de traitement sont même désactivées pour éviter les lacunes dans les preuves, au détriment de l'efficacité.

La deuxième contribution principale de cette thèse est un cadre pour résoudre ces problèmes.

C'est un travail en commun avec Jasmin Blanchette et Pascal Fontaine [START_REF] Barbosa | Scalable Fine-Grained Proofs for Formula Processing[END_REF]. Les preuves sont exprimées à l'aide d'un ensemble extensible de règles d'inférence (Chapitre 6). Les règles ont une granularité fine, permettant de séparer les théories ou même des lemmes différents de la même théorie. La clausification, les simplifications théoriques spécifiques et l'expansion des expressions "let" sont des exemples de ce cadre. La skolemisation peut sembler problématique, mais avec l'aide de l'opérateur de choix de Hilbert, elle peut également être intégrée au cadre.

Au coeur du cadre se trouve un algorithme de récurrence contextuelle générique qui traverse les termes à traduire (Chapitre 7). Le contexte fixe certaines variables, maintient une substitution et permet de suivre les polarités ou d'autres données. Le travail spécifique à la transformation, y compris la génération des preuves, est effectué par des fonctions de plugin qui sont données en xvi tant que paramètres du cadre. L'algorithme de récursivité, qui est essentiel pour la performance et l'exactitude des preuves générées, doit être implémenté une seule fois. Un autre avantage de l'architecture modulaire est que nous pouvons combiner facilement plusieurs transformations en une seule passe, sans compliquer le code ou compromettre le niveau de détail de la sortie de preuve.

Les règles d'inférence et l'algorithme de récurrence contextuelle bénéficient de nombreuses propriétés souhaitables. Nous montrons que les règles sont correctes et que le traitement des quantificateurs est correct même en présence de conflit dans les noms. De plus, en supposant des structures de données appropriées, nous montrons que la génération de preuves ajoute un coût proportionnel au temps passé à traiter les termes. Les preuves sont des graphes acycliques (DAG) et peuvent être produites avec une complexité de temps linéaire dans leur taille.

Nous avons mis en oeuvre l'approche également dans veriT, un solveur SMT. Le solveur est connu pour ses preuves détaillées [START_REF] Bouton | veriT: An Open, Trustable and Efficient SMT-Solver[END_REF], qui sont reconstruites dans les assistants de preuve Coq [START_REF] Armand | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses[END_REF] et Isabelle/HOL [START_REF] Christian Blanchette | Semi-intelligible Isar Proofs from Machine-Generated Proofs[END_REF]. En tant que preuve de concept, nous avons mis en place un prototype de checker dans Isabelle/HOL. En adoptant le nouveau cadre, nous avons pu supprimer de grandes quantités de code compliqué dans le solveur, tout en permettant des preuves détaillées pour plus de transformations qu'auparavant. L'algorithme de récurrence contextuelle devait être implémenté une seule fois et plus complètement testé que l'une quelconque des transformations monolithiques qu'il remplace. Notre évaluation empirique révèle que veriT est aussi rapide qu'avant, même s'il génère maintenant des preuves plus fines.

Résolution de satisfiabilité modulo des théories

La pertinence du problème SMT provient du gain considérable d'expressivité obtenu en combinant la logique du premier ordre avec les théories. Le raisonnement efficace dans un tel cadre est d'une importance capitale pour une variété d'applications formelles qui peuvent s'appuyer sur la logique pour coder des problèmes. Cela permet d'appliquer le raisonnement assisté par ordinateur, par exemple, la vérification formelle, la synthèse des programmes, les tests automatiques, l'analyse de programme, etc. L'accent mis sur les problèmes du monde réel impose une restriction aux solutions pertinentes à un problème SMT donné. On s'intéresse généralement uniquement à des solutions qui sont des extensions des modèles standard des théories d'arrière-plan. Donc dans la pratique, lors de la résolution, par exemple, d'un problème de satisfaction modulo l'arithmétique linéaire entière, les seules solutions souhaitées sont celles qui interprètent les symboles +, -, , etc., de la façon habituelle, et notamment sur le domaine des entiers. Un avantage de fixer des interprétations pour des théories, plutôt que de s'appuyer par exemple, sur des axiomatizations, est de pouvoir utiliser des procédures de décision ad hoc pour ces structures spécifiques, au lieu de s'appuyer sur des méthodes générales. Pour des combinaisons de théories sans quantification, cela conduit souvent à des procédures de décision hautement efficaces. xvii L'importance du problème SMT a conduit au domaine de la recherche communément connu comme "solution SMT" (voir [START_REF] Sebastiani | Lazy Satisability Modulo Theories[END_REF] ou [START_REF] Barrett | Satisfiability Modulo Theories[END_REF] pour des aperçus complets). Il est originaire du problème plus simple de satisfaction booléenne, c'est-à-dire déterminer si une formule propositionnelle a un modèle. Ce problème est communément connu sous le nom SAT, et est l'un des premiers à être montré NP-complet. En tant que tel, il s'agissait d'un problème insoluble pendant de nombreuses années, jusqu'à la révolution SAT au tournant du siècle dernier: les solveurs SAT modernes, mettant en oeuvre le calcul de l'apprentissage par clause (CDCL) axé sur les conflits, peuvent résoudre efficacement des problèmes contenant des centaines de milliers de variables propositionnelles et des millions de clauses. La satisfaisabilité modulo théorie est apparue initialement dans les années 1970 et 1980 par des pionniers tels que Nelson et Oppen [START_REF] Nelson | Simplification by Cooperating Decision Procedures[END_REF][START_REF] Nelson | Fast Decision Procedures Based on Congruence Closure[END_REF] et Shostak [START_REF] Shostak | Deciding Combinations of Theories[END_REF]. L'accent a été mis sur les logiques sans quantificateur, qui sont souvent décidables. Les approches modernes ont débuté à la fin des années 1990, exploitant la puissance des solveurs SAT pour construire des systèmes plus évolutifs. Ces approches peuvent être classées en deux grandes classes. Dans le premier cas, un problème SMT est entièrement codé dans une instance SAT et fourni à un solveur SAT, sans autre intervention. Le raisonnement au niveau théorie n'est effectué que pour fournir un meilleur encodage dans SAT. Dans le second cas, le raisonnement au niveau théorie est effectué par une combinaison de procédures de décision qui sont entrelacées avec un solveur SAT. Le problème SMT est généré par le SAT solveur, qui fournit une solution qui n'est qu'un candidat pour le problème d'origine. Le cadre CDCL(T ) [START_REF] Nieuwenhuis | Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)[END_REF] est une telle approche pour la résolution de SMT. C'est l'approche la plus commune adoptée dans les solveurs SMT actuels. Nous nous plaçons dans ce cadre avec comme objectif de raisonner ausi sur des formules quantifiées.

Dans les logiques classiques, le double problème de satisfaction est celui de la démonstration du théorème: montrer qu'une formule est un théorème équivaut à montrer que sa négation est insatisfaisante, tout en trouvant un modèle pour sa négation fournit un contre-exemple à la conjecture. Le champ de la démonstration automatique de théorème (ATP) historiquement était axé sur la logique du premier ordre pure avec égalité, où le plus grand défi consiste à gérer efficacement les formules quantifiées. Le raisonnement avec des théories et en présence de quantificateurs pose des défis majeurs, car il est souvent incomplet et difficile à réaliser efficacement, même de manière heuristique. Néanmoins, de nombreux travaux ont tenté d'étendre les systèmes ATP avec des théories, au point que les différences entre les solveurs SMT et les systèmes ATP deviennent de plus en plus petites.

Dans la Section 3.1, nous détaillons le calcul CDCL(T ). CDCL(T ) est une extension du calcul de l'apprentissage par clause de conflit (CDCL) qui intègre le raisonnement avec des théories. CDCL est un raffinement de la procédure classique DPLL [START_REF] Davis | A Machine Program for Theorem-proving[END_REF] qui combine une recherche en arrière pour un modèle propositionnel avec un puissant moteur d'analyse de conflit.

La recherche s'effectue en entrelacant les "décisions", c'est-à-dire l'attribution heuristiques de valeur de vérité à des propositions, avec l'application de la propagation unitaire jusqu'à un point fixe. Le retour arrière explicite est effectué au moyen d'une clause apprise dérivée lorsqu'un xviii conflit est atteint dans la recherche. La Section ?? détaille CDCL(T ), qui étend ceci dans le cadre SMT. En présence de quantificateurs, le problème satisfaisabilité modulo théorie est souvent coûteux, voir indécidable (en fonction de la théorie). Historiquement, dans le cadre CDCL(T ), des techniques d'instanciation heuristiques ont été utilisées pour résoudre ce problème.

Elles permettent de dériver rapidement des instances de base des quantificateurs et de ramener le raisonnement au niveau du solveur sans quantificateur. Nous décrivons ici les principales techniques d'instanciation appliquées dans CDCL(T ).

Instantiation

Production de preuves pour le traitement des formules

Un nombre croissant de prouveurs de théorèmes automatiques peuvent générer des certificats, ou des preuves, qui justifient les formules qu'ils dérivent. Ces preuves peuvent être vérifiées par d'autres programmes et partagées entre les systèmes de raisonnement. Certains utilisateurs voudront également inspecter ces sorties pour comprendre pourquoi une formule est valide. La production de preuve est généralement bien comprise pour les méthodes de preuve de base et pour de nombreuses théories couramment utilisées en SMT. Mais la plupart des prouveurs automatiques effectuent également un traitement ou un prétraitement de formule -comme la clausification et la réécriture avec des lemmes spécifiques à la théorie -et la production de xix Extended Abstract in French preuve pour cet aspect est moins mature.

Pour la plupart des prouveurs, le code pour les formules de traitement est long et traite d'une multitude de cas, dont certains sont rarement exécutés. Bien qu'il soit crucial pour l'efficacité, ce code tend à recevoir beaucoup moins d'attention que d'autres aspects des prouveurs. Les développeurs sont réticents à investir de l'énergie pour produire des preuves détaillées pour un tel traitement, car cela nécessite d'adapter beaucoup de code. En conséquence, la granularité des inférences pour le traitement de la formule est souvent grossière. Parfois, les fonctionnalités de traitement sont même désactivées pour éviter les lacunes dans les preuves, à un coût élevé dans la performance de la recherche de preuve.

Les preuves à grain fin sont importantes pour diverses applications. Nous proposons un cadre pour générer de telles preuves sans ralentir la recherche de preuve. Le Chapitre 6 décrit un calcul de preuve dans lequel générer des preuves fines pour traiter des formules. Le chapitre 7 présente un cadre évolutif pour générer de telles preuves. Les deux chapitres décrivent le travail commun avec Jasmin Blanchette et Pascal Fontaine [START_REF] Barbosa | Scalable Fine-Grained Proofs for Formula Processing[END_REF].

Nous proposons un algorithme générique pour les transformations de termes, basé sur la récurrence structurale. L'algorithme est paramétré par quelques fonctions de plugin simples incorporant l'essence de la transformation. En combinant des fonctions de plugin compatibles, nous pouvons effectuer plusieurs transformations dans une traversée. Les transformations peuvent dépendre d'un contexte qui encapsule les informations pertinentes, telles que les variables liées, les substitutions variables et la polarité. Chaque transformation peut définir sa propre notion de contexte qui est traversée par la récurrence.

La sortie est générée par un module de preuve qui maintient une pile d'arbres de dérivation.

La procédure apply(R, n, Γ, t, u) retire n arbres de dérivation Dn de la pile et ajoute l'arbre

D 1 • • • D n R Γ t u
E |= ¬ψ 1 σ ∨ • • • ∨ ¬ψ n σ, avec Q = {∀x. ψ 1 , . . . , ∀x.

Extended Abstract in Portuguese

Introdução

Em muitas aplicações de métodos formais, como verificação formal, síntese de programas, testes automáticos e análise de programas, é comum depender de lógicas para representar condições que precisam ser verificadas. Essas condições geralmente podem ser reduzidas para o problema Satisfatibilidade Módulo Teorias (SMT) (Capítulo 2): dada uma fórmula em lógica de primeira ordem, ela possui um modelo consistente com uma combinação de teorias? Os solucionadores SMT tornaram-se, assim, recursos populares para ferramentas que automatizam a verificação formal, a síntese de programas e assim por diante. Eles eliminam automaticamente as obrigações de prova -condições a severificar -e fornecem certificados de seus resultados, ou seja, modelos ou demonstrações. Nesta tese, objetivamos melhorar a eficiência dos solucionadores SMT e aumentar sua confiabilidade.

Os solucionadores SMT (Capítulo 3) foram projetados principalmente para resolver problemas sem quantificadores, nos quais eles são altamente eficientes e capazes de lidar com grandes fórmulas contendo símbolos interpretados. A lógica de primeira ordem pura quantificada é melhor tratada com técnicas baseadas em resolução e superposição [START_REF] Bachmair | Rewrite-Based Equational Theorem Proving with Selection and Simplification[END_REF][START_REF] Nieuwenhuis | Paramodulation-Based Theorem Proving[END_REF]. Embora existam tentativas [START_REF] De | Engineering DPLL(T) + Saturation[END_REF] em unificar tais técnicas com CDCL(T ) [START_REF] Nieuwenhuis | Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)[END_REF], o cálculo que os solucionadores SMT geralmente implementam, a abordagem mais comum ainda é instanciação: as fórmulas quantificadas são reduzidas a fórmulas sem quantificadores e refutadas com a ajuda de procedimentos de decisão para tais fórmulas. As principais técnicas de instanciação são E -matching, com base em gatilhos [DNS05, dMB07, Rüm12], procura de instâncias conflitantes [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF] e instanciação de quantificadores baseada em modelos (MBQI) [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF][START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF]. Cada uma dessas técnicas contribui para a eficiência de solucionadores de última geração, mas cada uma delas é tipicamente implementada de forma independente.

Apresentamos o problema de E-ground (dis)unification como a base de um arcabouço único no qual todas essas técnicas podem ser acomodadas (Capítulo 4). Este problema relaciona-se com o problema clássico de E -unification [START_REF] Degtyarev | What You Always Wanted to Know about Rigid E-Unification[END_REF] e é também NP-completo. Resolver o problema de E-ground (dis)unification equivale a encontrar substituições de modo que os literais que contenham variáveis livres sejam válidos de acordo com os literais sem variáveis atualmente no contexto. Uma vez que o domínio de instanciação dessas variáveis pode ser delimitado, uma possível maneira de resolver o problema é adivinhar, de forma não determinista, uma substituição xxiv e verificar se ela é uma solução. O algoritmo Fechamento de Congruência com Variáveis Livres (CCFV, abreviado) apresentado aqui é um procedimento de decisão para este problema na prática, baseado no algoritmo clássico de fechamento de congruência [START_REF] Nelson | Fast Decision Procedures Based on Congruence Closure[END_REF][START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF]. É um procedimento orientado por objetivos: as soluções são construídas de forma incremental, levando em consideração o fechamento de congruência dos termos definidos pelas igualdades no contexto e as possíveis atribuições às variáveis. Nós então mostramos como se basear no CCFV para implementar as técnicas de instanciação baseadas em gatilhos, conflitos e modelos (Capítulo 5).

Uma avaliação experimental é apresentada, na qual medimos o impacto das otimizações e técnicas de instanciação baseadas no CCFV. Mostramos que nossas implementações exibem melhorias em relação às abordagens de última geração. Este trabalho levou a uma publicação conjunta com Pascal Fontaine e Andrew Reynolds [START_REF] Barbosa | Congruence Closure with Free Variables[END_REF].

Técnicas de instanciação para SMT vem sendo amplamente estudadas. A instanciação heurística baseada em E -matching dos gatilhos selecionados foi introduzida por Nelson [START_REF] Gregory | Techniques for Program Verification[END_REF] e foi implementada com sucesso em vários solucionadores. Uma implementação altamente eficiente de E -matching no contexto de solucionadores SMT foi apresentada por Moura e Bjørner [START_REF] De | Efficient E-Matching for SMT Solvers[END_REF]; baseia-se em algoritmos incrementais de matching, geração de código de máquina para otimizar o desempenho e elaboradas técnicas de indexação combinando recursos comuns em índices para demonstradores de teoremas baseados em saturação. Rümmer usa gatilhos junto com um método clássico de tableaux [START_REF] Rümmer | E-Matching with Free Variables[END_REF]. A instanciação baseada em gatilhos, infelizmente, produz muitas instâncias irrelevantes. Para enfrentar este problema, uma técnica de instanciação orientada por objetivos que produz apenas instâncias relevantes foi apresentada por Reynolds et al. [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF].

CCFV possuis semelhanças com este algoritmo, com sua busca sendo baseada na estrutura de termos e em um modelo atual proveniente do solucionador sem quantificaderos. A abordagem aqui é, no entanto, mais geral, da qual esta técnica anterior é uma especialização. A instanciação de quantificadores baseada em modelos (MBQI) de Ge e de Moura (MBQI) [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF] fornece um método completo para a lógica de primeira ordem através da derivação sucessiva de instâncias conflitantes para refinar um candidato a modelo para toda a fórmula, incluindo quantificadores.

Ele permite ao solucionador encontrar modelos finitos quando estes existem. A verificação do modelo é realizada com uma cópia separada do solucionador SMT em busca de uma instância conflitante. Métodos alternativos para a construção e verificação do modelo foram apresentados por Reynolds et al. [START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF]. Essas abordagens baseadas em modelos [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF][START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF] permitem a integração de teorias além da igualdade, enquanto que CCFV por enquanto apenas lida com igualdade e funções não interpretadas. Backeman e Rümmer resolvem o problema relacionado de E -unification através da sua codificação em SAT, usando um solucionador SAT off-the-shelf para calcular soluções [START_REF] Backeman | Theorem Proving with Bounded Rigid E-Unification[END_REF]. Nosso trabalho está mais em linha com técnicas como as de Goubault [START_REF] Goubault | A rule-based algorithm for rigid E-unification[END_REF] e Tiwari et al. [START_REF] Tiwari | Rigid E-Unification Revisited[END_REF], orientadas por objetivos; uma vez que os algoritmos de fechamento de congruência são muito eficientes na verificação de soluções, acreditamos que eles também podem ser o núcleo de algoritmos eficientes para descobri-las. CCFV difere das técnicas anteriores de forma notável, já que lida com desigualdades e que restringe xxv Extended Abstract in Portuguese a busca de soluções com base na estrutura de um modelo para a fórmula sem quantificadores, sendo portanto mais adequada para um contexto SMT.

Um aspecto muito importante no raciocínio automatizado é fornecer certificados para os resultados produzidos que possam ser verificados por máquinas. As aplicações externas que utilizam sistemas automáticos geralmente não precisam apenas das respostas ao problema de satisfação, mas também de suas justificativas. Por exemplo, ao se tentar verificar se um teorema é válido através da demonstração de que sua negação é insatisfatível, produzir um modelo caso a fórmula seja satisfatível fornece um contra-exemplo para a conjectura. Além disso, uma vez que esses solucionadores podem ser sistemas com uma engenharia bastante complexa, muitas vezes com centenas de milhares de linhas de código, é difícil garantir que as implementações sejam livres de erros. Portanto, ser capaz de verificar os resultados produzidos é de suma importância para melhorar a confiabilidade de qualquer dessas ferramentas.

Um número crescente de demonstradores automáticos de teoremas pode gerar certificados ou demonstrações que justifiquem seus resultados. Essas demonstrações podem ser verificadas por outros programas e compartilhadas entre sistemas de raciocínio. A produção de demonstrações geralmente é bem compreendida para os métodos principais de demonstração (por exemplo, superposição, tableaux, aprendizagem de cláusulas orientada por conflitos) e para muitas teorias comumente usadas em SMT. No entanto, a maioria dos demonstradores automáticos também realizam algum processamento ou pré-processamento de fórmulas -por exemplo clausificação e reescrita com lemas específicos de teorias -e a produção de demonstrações para estas técnicas é menos madura. Para a maioria dos demonstradores, o código para processamento de fórmulas não é particularmente complicado, mas é longo e lida com uma infinidade de casos, alguns dos quais raramente são executados. Embora seja crucial para a eficiência, este código tende a receber muito menos atenção do que outros aspectos dos demonstradores. Os desenvolvedores são relutantes em investir esforço na produção de demonstrações detalhadas para esse processamento, pois isso requer a adaptação de uma grande quantidade de código. Como resultado, a granularidade das inferências para o processamento da fórmula é muitas vezes grosseira. Às vezes, os recursos de processamento são até desativados para evitar lacunas nas demonstrações, com alto custo no desempenho da procura de demonstrações.

A segunda contribuição principal desta tese é um arcabouço para abordar lidar com esses problemas. Este trabalho levou a uma publicação conjunta com Jasmin Blanchette e Pascal Fontaine [START_REF] Barbosa | Scalable Fine-Grained Proofs for Formula Processing[END_REF]. As demonstrações são expressadas usando um conjunto extensível de regras de inferência (Capítulo 6). As regras têm uma granularidade fina, possibilitando uma clara separação entre teorias ou até mesmo lemmas diferentes da mesma teoria. Clausificação, simplificações específicas de teorias e expansão das expressões de "let" são exemplos de técnicas acomodadas neste arcabouço. A Skolemização pode parecer problemática, mas com a ajuda do operador de escolha de Hilbert ela também pode ser integrada no arcabouço. No coração do arcabouço encontra-se um algoritmo genérico de recursão contextual que atravessa os termos a serem processados (Capítulo 7). O contexto fixa algumas variáveis, mantém uma substituição e xxvi acompanha as polaridades ou outros dados. O trabalho específico de transformação, incluindo a geração de demonstrações, é executado por funções plugáveis que são fornecidas como parâmetros para o arcabouço. O algoritmo de recursão, que é crítico para o desempenho e a correção das demonstrações produzidas, precisa ser implementado apenas uma vez. Outro benefício da arquitetura modular é que podemos combinar facilmente várias transformações em uma única passagem, sem complicar indevidamente o código ou comprometer o nível de detalhe da demonstração produzida.

As regras de inferência e o algoritmo de recursão contextual possuem muitas propriedades desejáveis. Mostramos que as regras são corretas e que o tratamento de binders é correto mesmo na presença de conflitos de nomes. Além disso, assumindo estruturas de dados adequadas, mostramos que a geração de demonstrações cria apenas uma sobrecarga que é proporcional ao tempo gasto no processamento dos termos. A verificação de demonstrações representadas como grafos direcionadas acíclicos (DAGs) pode ser realizada com uma complexidade de tempo que é linear em seu tamanho. Implementamos a abordagem também no solucionador SMT veriT. O solucionador é conhecido por suas demonstrações detalhadas [START_REF] Bouton | veriT: An Open, Trustable and Efficient SMT-Solver[END_REF], que são reconstruídas nos assistentes de demonstração Coq [START_REF] Armand | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses[END_REF] e Isabelle/HOL [START_REF] Christian Blanchette | Semi-intelligible Isar Proofs from Machine-Generated Proofs[END_REF]. Para validar o conceito, implementamos um protótipo para checagem em Isabelle/HOL. Ao adotar o novo arcabouço, conseguimos remover grandes quantidades de código complicado no solucionador, ao mesmo tempo em que permitimos a produção de demonstrações detalhadas para mais transformações do que antes.

O algoritmo de recursão contextual teve que ser implementado apenas uma vez e é testado de forma mais completa do que qualquer uma das transformações monolíticas que ele substitui.

Nossa avaliação empírica revela que veriT é tão rápido quanto antes, embora ele agora gere demonstrações de melhor qualidade.

Resolução de satisfatibilidade módulo teorias

A relevância do problema SMT vem do ganho considerável de expressividade alcançado pela combinação de lógica de primeira ordem com teorias. Raciocinar de forma eficiente em tal cenário é de extrema importância para uma variedade de métodos formais que podem depender de lógica para codificar problemas. Isso permite que o raciocínio assistido por computador seja aplicado em, por exemplo, verificação formal, síntese de programas, testes automáticos, análise de programas e assim por diante.

O foco em problemas do mundo real impõe uma restrição às soluções relevantes para um determinado problema SMT. Geralmente busca-se apenas soluções que são extensões dos modelos padrão das teorias. Então, na prática, ao resolver, por exemplo, um problema de satisfação módulo aritmética linear com inteiros, as únicas soluções desejadas são aquelas que interpretam os símbolos +, -, <, etc., da maneira usual, no domínio dos inteiros. Um benefício de fixar interpretações para teorias, ao invés de depender por exemplo de axiomatizações, é poder usar procedimentos (de decisão) ad-hoc para essas estruturas específicas, em vez de depender de métodos de propósito geral. Para combinações de teorias livres de quantificadores, isto geralmente leva a procedimentos de decisão altamente eficientes.

A importância do problema SMT levou ao campo de pesquisa comumente conhecido como "Resolução SMT" (veja [START_REF] Sebastiani | Lazy Satisability Modulo Theories[END_REF] ou [START_REF] Barrett | Satisfiability Modulo Theories[END_REF] para obter mais detalhes). Ele se originou com o problema mais simples de satisfatibilidade Booleana, isto é, determinar se uma fórmula proposicional possui um modelo. Este problema é comumente conhecido como SAT, e é um dos primeiros demonstrados ser NP-completo. Como tal, foi um problema intratável por muitos anos, até a chamada revolução SAT na virada do século passado: os modernos solucionadores SAT, implementando o cálculo de aprendizagem de cláusulas orientada por conflitos (CDCL), podem resolver de forma eficiente problemas muito grandes provenientes de problemas do mundo real contendo centenas de milhares de variáveis proposicionais e milhões de cláusulas. A resolução SMT foi desenvolvida inicialmente nos anos 1970 e 1980 por pioneiros como Nelson e Oppen [START_REF] Nelson | Simplification by Cooperating Decision Procedures[END_REF][START_REF] Nelson | Fast Decision Procedures Based on Congruence Closure[END_REF] e Shostak [START_REF] Shostak | Deciding Combinations of Theories[END_REF]. O foco desde então foi geralmente em lógicas livres de quantificadores, que são muitas vezes decidíveis. As abordagens modernas começaram no final da década de 1990, aproveitando o poder dos solucionadores SAT para construir sistemas com maior escalabilidade.

Essas abordagens podem ser classificadas em duas grandes classes. Na primeiro, um problema SMT é totalmente codificado em uma instância SAT e resolvido com um solucionador SAT, sem intervenção adicional. O raciocínio para teorias é realizado apenas para fornecer uma melhor codificação para SAT. Na segunda, o raciocínio para teorias é realizado por uma combinação de procedimentos de decisão que são intercalados com um solucionador SAT. O problema SMT é abstraído como uma instância SAT, cuja solução é apenas uma candidata para o problema original: uma conjunção proposicionalmente consistente de literais, que é então verificada de acordo com a consistência módulo teorias. O arcabouço CDCL(T ) [START_REF] Nieuwenhuis | Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)[END_REF] é uma abordagem para a resolução SMT. É o mais comum adotado para sistemas que executam a resolução SMT automática. Nosso foco é neste arcabouço e, mais importante ainda, sobre como raciocinar de forma eficiente com fórmulas quantificadas nele. Na lógica clássica, o duplo problema da satisfação é o da demonstração de teoremas: mostrar que uma fórmula é um teorema é equivalente a mostrar que sua negação é insatisfatível, ao encontrar um modelo para a sua negação fornece-se um contra-exemplo para a conjectura. O campo de demonstração automática de teoremas (ATP) historicamente foi focado em lógica de primeira ordem pura e equacional, onde o maior desafio é como gerenciar eficientemente fórmulas quantificadas. O raciocínio de teorias na presença de quantificadores traz grandes desafios, pois muitas vezes é incompleto e difícil de ser realizado de forma eficiente, mesmo de forma heurística.

No entanto, inúmeros trabalhos tentaram estender os sistemas ATP com raciocínio de teorias, ao ponto de as diferenças entre solucionadores SMT e sistemas ATP serem cada vez menores. Na Seção 3.1 detalhamos o cálculo CDCL(T ), que é uma extensão do cálculo de aprendizagem de cláusulas de conflito (CDCL) que acomoda o raciocínio de teorias. CDCL é um refinamento do clássico procedimento DPLL [START_REF] Davis | A Machine Program for Theorem-proving[END_REF] que combina um poderoso mecanismo de análise de xxviii conflitos com a busca, baseada em backtracking de um modelo proposicional. A busca é realizada através da intercalação de "decisões", ou seja, atribuições heurísticas de literais, com a aplicação de propagação de unidade até um ponto fixo. Backtracking é realizada de forma explícita por meio de uma cláusula aprendida derivada quando um conflito é atingido na busca. A Seção 3.2 detalha o raciocínio com quantificadores em CDCL(T ). Raciocinar com quantificadores na presença de teorias é muitas vezes dispendioso e em geral indecidível. Historicamente, no arcabouço CDCL(T ), geralmente técnicas de instanciação heurística foram usadas para enfrentar esse problema. Elas permitem derivar rapidamente as instâncias dos quantificadores e transferir o raciocínio de volta para o eficiente solucionador livre de quantificadores. Aqui descrevemos as principais técnicas de instanciação aplicadas em CDCL(T ).

Instanciação

Um problema central ao aplicar técnicas de instanciação em CDCL(T ) é como determinar quais instâncias derivar. Cada uma das principais técnicas, seja a baseada em gatilhos, conflitos ou modelos, contribui muito para a eficiência de solucionadores de última geração, mas cada uma delas é tipicamente implementada de forma independente e ad hoc em seus próprios arcabouços.

No Capítulo 4 apresentamos um arcabouço uniforme para o raciocínio com fórmulas quantificadas em CDCL(T ) na teoria da igualdade e funções não interpretadas. Apresentamos o problema E-ground (dis)unification como a base deste arcabouço (Seção 4.1), em que as técnicas de instanciação baseadas em gatilhos, conflitos e modelos podem ser acomodadas. Este problema relaciona-se com o problema clássico de E -unification [START_REF] Degtyarev | What You Always Wanted to Know about Rigid E-Unification[END_REF], pervasivo em cálculos para lógica equacional de primeira ordem baseados em sequentes e tableaux. Ao explorar as semelhanças entre CDCL(T ) e esses arcabouços, nos baseamos em técnicas convencionais para solucionar E -unification e apresentamos um procedimento de decisão para E-ground (dis)unification: Fechamento de Congruência com Variáveis Livres (CCFV, abreviado), que estende o clássico algoritmo de fechamento de congruência [NO80, NO07], para acomodar variáveis livres (Seção 4.2).

Em seguida, mostramos como se basear em CCFV para executar instanciações baseadas em gatilhos, conflitos e modelos. Um relatório detalhado da implementação e avaliação experimental de CCFV e as técnicas de instanciação em torno dele é apresentada no Capítulo 5.

Produção de demonstrações para o processamento de fórmulas

Um número crescente de demonstradores automáticos de teorema pode gerar certificados ou demonstrações que justifiquem seu funcionamento. Essas demonstrações podem ser verificadas por outros programas e compartilhadas entre sistemas de raciocínio. Alguns usuários também querem inspecionar estes resultados para entender por que uma fórmula é válida. A produção de demonstrações geralmente é bem compreendida para os principais métodos de demonstração e para muitas teorias comumente usadas em SMT. Mas a maioria dos demonstradores automáticos xxix Extended Abstract in Portuguese também executam algum processamento ou pré-processamento de fórmulas -como clausificação e reescrita com lemas específicos de teorias -e a produção de demonstração para este aspecto é menos madura. Para a maioria dos demonstradores, o código para processamento de fórmulas é longo e lida com uma infinidade de casos, alguns dos quais raramente são executados. Embora seja crucial para a eficiência, este código tende a receber muito menos atenção do que outros aspectos dos provers. Os desenvolvedores são relutantes em investir tempo na produção de demonstrações detalhadas para esse processamento, pois isso requer a adaptação de muito código. Como resultado, a granularidade das inferências para o processamento da fórmula é muitas vezes grosseira.

Às vezes, os recursos de processamento são até desativados para evitar lacunas nas provas, com alto custo no desempenho da procura de prova.

As provas de granularidade fina são importantes para uma variedade de aplicações. Propomos um arcabouço para gerar tais demonstrações sem desacelerar a busca por demonstrações. O Capítulo 6 descreve um cálculo de demonstrações com o qual gerar demonstrações detalhadas para o processamento de fórmulas. O Capítulo 7 apresenta um arcabouço escalável para gerar tais demonstrações.

Propomos um algoritmo genérico para transformações de termos, com base em recursão estrutural. O algoritmo é parametrizado por algumas funções plugáveis simples que incorporam a essência da transformação. Ao combinar funções plugáveis compatíveis, podemos realizar várias transformações em uma única passagem. As transformações podem depender de algum contexto que encapsula informações relevantes, como variáveis fixadas, substituições de variáveis e polaridade. Cada transformação pode definir sua própria noção de contexto que é transmitida através da recursão.

O resultado é gerado por um módulo de demonstração que mantém uma pilha de árvores de derivações. O procedimento apply(R, n, Γ, t, u) retira n árvores de derivação Dn da pilha e insere a árvore CCFV pode ser visto como um primeiro passo para um "solucionador de teorias" para fórmulas quantificadas a ser integrado em um solucionador CDCL(T ). As técnicas de instanciação baseadas em CCFV avaliariam o modelo candidato com fórmulas quantificadas e iriam: i) fornecer um modelo finito quando existisse, ii) derivar instâncias refutando o candidato quando existissem, iii) propagar instâncias relevantes e iv) ser incremental em relação às atribuições proposicionais.

D 1 • • • D n R Γ t
A incrementalidade depende da implementação de CCFV. A instanciação baseada em conflitos contempla parcialmente (ii) e (iii), enquanto a instanciação baseada em gatilhos se encaixa em (iii) e instanciação baseada em modelos um pouco em (i) e (ii). Como estender as técnicas de instanciação para atingir esses objetivos permanece um problema em aberto. Uma técnica completa de instanciação baseada em conflito, pelo menos em relação à lógica equacional de primeira ordem, poderia ser alcançada considerando fórmulas quantificadas simultaneamente em vez de independentemente, isto é, encontrando substituições sigma tal que

E |= ¬ψ 1 σ ∨ • • • ∨ ¬ψ n σ, with Q = {∀x. ψ 1 , . . . , ∀x. ψ n }
Técnicas de tableaux e cálculos de superposição, que nativamente consideram fórmulas quantificadas simultaneamente, poderiam ser combinadas com CCFV para resolver o problema acima.

Nossa segunda contribuição foi apresentar um arcabouço para representar e gerar demonstrações do processamento de fórmulas e sua implementação em veriT e Isabelle/HOL. A estrutura centraliza a sutil questão de manipular variáveis vinculadas e substituições de forma correta e eficiente, e é flexível o suficiente para acomodar muitas transformações interessantes. Embora tenha sido implementado em um solucionador SMT, parece não haver uma limitação intrínseca que evite seu uso em outros tipos de demonstradores automáticos de primeira ordem, ou mesmo de ordem superior. O arcabouço cobre muitas técnicas de pré-processamento e pode ser parte de uma caixa de ferramentas maior. Ele permite que veriT, cujas demonstrações detalhadas tem sido uma de suas características definidoras, possa produzir justificativas mais detalhadas do que nunca. No entanto, ainda existem algumas transformações globais para as quais as demonstrações são inexistentes ou deixam muito a desejar. Para lidar com essas transformações nossa noção de contexto teria que ser estendida, bem como as operações que podem ser realizadas em termos, de tal forma que possamos ir além da substituição de iguais por iguais. A estrutura também pode ser estendida para lidar com diferentes construções de linguagem, como abstrações com lambdas. Dada a generalidade do cálculo de processamento e o algoritmo de produção de demonstrações, as operações como redução beta podem ser facilmente integradas. O último, por exemplo, é apenas uma variação da expansão de "let". xxxii Nosso foco aqui tem sido a produção de demonstrações detalhadas, com o objetivo de garantir que a verificação de demonstrações tenha uma complexidade razoável e assim facilitar a implementação efetiva de verificadores. Uma direção promissora é também reconstruir as demonstrações detalhadas em assistentes de demonstração, que fornecem demonstrações formais de teoremas que são confiáveis e verificáveis por máquinas. Um desafio geral é executar dentro dos assistentes de demonstração o raciocínio necessário para verificar as demonstrações. Para algumas teorias, como a aritmética não linear, isso pode ser bastante desafiador. Uma vez possível, a reconstrução total de demonstrações em assistentes de demonstração aumentaria consideravelmente a confiança geral sobre os resultados de solucionadores automáticos, evitando assim a necessidade de se confiar em programas que dependem principalmente de testes para executar raciocínio lógica de forma correta.

Para concluir, acreditamos que nossas contribuições são benéficas para o estado-da-arte da resolução SMT (e, conseqüentemente, também da demonstração de teorema em lógica de primeira ordem). Além disso, uma vez que ambos os arcabouços apresentados são bastante gerais e extensíveis, esperamos que eles sirvam como ponto de partida para várias outras técnicas de instanciação e produção de demonstrações na resolução SMT, tornando solucionadores capazes de enfrentar problemas cada vez mais expressivos e produzindo resultados mais confiáveis.

Chapter 1

Introduction

In many formal methods applications, such as formal verification, program synthesis, automatic testing, and program analysis, it is common to rely on logics to represent conditions that need to be asserted. These conditions can often be reduced to the Satisfiability Modulo Theories (SMT) problem (Chapter 2): given a first-order logic formula, does it have a model consistent with a combination of background theories? SMT solvers have thus become popular backends for tools automating formal verification, program synthesis and so on. They automatically discharge proof obligations -conditions to be checked -and provide certificates of their results, i.e. models or proofs. In this thesis we aim both to improve the efficiency of SMT solvers and to increase their reliability.

SMT solvers (Chapter 3) have been primarily designed to solve quantifier-free problems, on which they are highly efficient and capable of handling large formulas with interpreted symbols.

Pure quantified first-order logic is best handled with resolution and superposition based theorem proving [START_REF] Bachmair | Rewrite-Based Equational Theorem Proving with Selection and Simplification[END_REF][START_REF] Nieuwenhuis | Paramodulation-Based Theorem Proving[END_REF]. Although there are first attempts [START_REF] De | Engineering DPLL(T) + Saturation[END_REF] to unify such techniques with CDCL(T ) [START_REF] Nieuwenhuis | Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)[END_REF], the calculus that SMT solvers usually implement, the most common approach is still instantiation: quantified formulas are reduced to ground ones and refuted with the help of decision procedures for ground formulas. The main instantiation techniques are Ematching based on triggers [START_REF] Detlefs | Simplify: A Theorem Prover for Program Checking[END_REF][START_REF] De | Efficient E-Matching for SMT Solvers[END_REF][START_REF] Rümmer | E-Matching with Free Variables[END_REF], finding conflicting instances [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF] and model based quantifier instantiation (MBQI) [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF][START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF]. Each of these techniques contributes to the efficiency of state-of-the-art solvers, yet each one is typically implemented independently.

We introduce the E-ground (dis)unification problem as the cornerstone of a unique framework in which all these techniques can be cast (Chapter 4). This problem relates to the classic problem of rigid E -unification [START_REF] Degtyarev | What You Always Wanted to Know about Rigid E-Unification[END_REF] and is also NP-complete. Solving E-ground (dis)unification amounts to finding substitutions such that literals containing free variables hold in the context of currently asserted ground literals. Since the instantiation domain of those variables can be bound, a possible way of solving the problem is by first non-deterministically guessing a substitution and checking if it is a solution. The Congruence Closure with Free Variables algorithm (CCFV, for short) presented here is a practical decision procedure for this problem based on the classic congruence closure algorithm [START_REF] Nelson | Fast Decision Procedures Based on Congruence Closure[END_REF][START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF]. It is goal-oriented: solutions are constructed incrementally, taking into account the congruence closure of the terms defined by the equalities in the context and the possible assignments to the variables. We then show how to build on CCFV to implement trigger based, conflict based and model based instantiation (Chapter 5). An experimental evaluation is presented, in which we measure the impact of optimizations and instantiation techniques based on CCFV. We show that our implementations exhibit improvements over state-of-the-art approaches. This work led to a joint publication with Pascal Fontaine and Andrew Reynolds [START_REF] Barbosa | Congruence Closure with Free Variables[END_REF].

Instantiation techniques for SMT have been extensively studied. Heuristic instantiation based on E -matching of selected triggers was first introduced by Nelson [Nel80] and has been successfully implemented in several solvers. A highly efficient implementation of E -matching in the context of SMT solvers was presented by de Moura and Bjørner [START_REF] De | Efficient E-Matching for SMT Solvers[END_REF]; it relies on incremental matching algorithms, generation of machine code for optimizing performance, and elaborated indexing techniques combining features common in indexes for saturation based theorem provers.

Rümmer uses triggers alongside a classic tableaux method [START_REF] Rümmer | E-Matching with Free Variables[END_REF]. Trigger based instantiation unfortunately produces many irrelevant instances. To tackle this issue, a goal-oriented instantiation technique producing only useful instances was introduced by Reynolds et al. [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF].

CCFV shares resemblance with this algorithm, since its search is also based on the structure of terms and the use of the model coming from the ground solver. The approach here is however more general, of which this previous technique is a specialisation. Ge and de Moura's model based quantifier instantiation (MBQI) [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF] provides a complete method for equational first-order logic and other fragments through successive derivation of conflicting instances to refine a candidate model for the whole formula, including quantifiers. It allows the solver to find finite models when they exist. Model checking is performed with a separate copy of the ground SMT solver searching for a conflicting instance. Alternative methods for model construction and checking were presented by Reynolds et al. [START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF]. Both these model based approaches [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF][START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF] allow integration of theories beyond equality, while CCFV for now only handles equality and uninterpreted functions. Backeman and Rümmer solve the related problem of rigid E -unification through encoding into SAT, using an off-the-shelf SAT solver to compute solutions [START_REF] Backeman | Theorem Proving with Bounded Rigid E-Unification[END_REF]. Our work is more in line with goal-oriented techniques as those by Goubault [Gou93] and Tiwari et al. [START_REF] Tiwari | Rigid E-Unification Revisited[END_REF]; congruence closure algorithms being very efficient at checking solutions, we believe they can also be the core of efficient algorithms to discover them. CCFV differs from those previous techniques notably, since it handles disequalities and since the search for solutions is pruned based on the structure of a ground model and is thus most suitable for an SMT context.

A very important aspect in automated reasoning is to provide machine checkable certificates for produced results. External applications using automatic systems generally need not only the answer to the satisfiability problem but also a justification. For example, when checking if a theorem is valid by trying to show that its negation is unsatisfiable, producing a model in the case a satisfiable formula provides a counter-example for the conjecture. Moreover, since these systems can be really complex engineering softwares, often with hundreds of thousands of lines of code, it is hard to ensure that implementations are free of errors. Therefore being able to verify the produced results is of paramount importance for improving the reliability of any such tool.

An increasing number of automatic theorem provers can generate certificates, or proofs, that justify their results. These proofs can be checked by other programs and shared across reasoning systems. Proof production is generally well understood for the core proving methods (e.g., superposition, tableaux, conflict-driven clause learning) and for many theories commonly used in satisfiability modulo theories (SMT). However, most automatic provers also perform some formula processing or preprocessing-such as clausification and rewriting with theory-specific lemmas-and proof production for this aspect is less mature. For most provers, the code for processing formulas is not particularly complicated, but it is lengthy and deals with a multitude of cases, some of which are rarely executed. Although it is crucial for efficiency, this code tends to be given much less attention than other aspects of provers. Developers are reluctant to invest effort in producing detailed proofs for such processing, since this requires adapting a lot of code.

As a result, the granularity of inferences for formula processing is often coarse. Sometimes, processing features are even disabled to avoid gaps in proofs, at a high cost in proof search performance.

The second main contribution of this thesis is a framework to address these issues. This work led to a joint publication with Jasmin Blanchette and Pascal Fontaine [START_REF] Barbosa | Scalable Fine-Grained Proofs for Formula Processing[END_REF]. Proofs are expressed using an extensible set of inference rules (Chapter 6). The succedent of a rule is an equality between the original term and the translated term. (It is convenient to consider formulas as a special case of terms.) The rules have a fine granularity, making it possible to cleanly separate theories or even different lemmas from the same theory. Clausification, theory-specific simplifications, and expansion of 'let' expressions are instances of this framework. Skolemization may seem problematic, but with the help of Hilbert's choice operator, it can also be integrated into the framework. Some provers provide very detailed proofs for parts of the solving, but we are not aware of any publications about practical attempts to provide easily reconstructible proofs for processing formulas containing quantifiers and 'let' expressions. At the heart of the framework lies a generic contextual recursion algorithm that traverses the terms to translate (Chapter 7).

The context fixes some variables, maintains a substitution, and keeps track of polarities or other data. The transformation-specific work, including the generation of proofs, is performed by plugin functions that are given as parameters to the framework. The recursion algorithm, which is critical for the performance and correctness of the generated proofs, needs to be implemented only once. Another benefit of the modular architecture is that we can easily combine several transformations in a single pass, without unduly complicating the code or compromising the level of detail of the proof output.

The inference rules and the contextual recursion algorithm enjoy many desirable properties.

Chapter 1. Introduction

We show that the rules are sound and that the treatment of binders is correct even in the presence of name clashes. Moreover, assuming suitable data structures, we show that proof generation adds an overhead that is proportional to the time spent processing the terms. Checking proofs represented as directed acyclic graphs (DAGs) can be performed with a time complexity that is linear in their size.

We implemented the approach also in the SMT solver veriT. The solver is known for its detailed proofs [BdODF09, BFT11, DFP11], which are reconstructed in the proof assistants Coq [START_REF] Armand | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses[END_REF] and Isabelle/HOL [START_REF] Christian Blanchette | Semi-intelligible Isar Proofs from Machine-Generated Proofs[END_REF]. As a proof of concept, we implemented a prototype checker in Isabelle/HOL. By adopting the new framework, we were able to remove large amounts of complicated code in the solver, while enabling detailed proofs for more transformations than before. The contextual recursion algorithm had to be implemented only once and is more thoroughly tested than any of the monolithic transformations it subsumes. Our empirical evaluation reveals that veriT is as fast as before even though it now generates finer-grained proofs.

Chapter 2

Conventions and definitions

We introduce here the logical framework and conventions used throughout this thesis. Our setting is a many-sorted classical first-order logic with equality (see e.g. Fitting [START_REF] Fitting | First-Order Logic and Automated Theorem Proving[END_REF] or Baader and Nipkow [START_REF] Baader | Term Rewriting and All That[END_REF] for general accounts), as defined by the SMT-LIB standard [START_REF] Barrett | The SMT-LIB Standard: Version 2.5[END_REF]. We introduce below the syntax and semantics we rely on in our work on satisfiability checking modulo theories.

Syntax

Definition 2.1 (Many-sorted first-order language). Given disjoint countably infinite sets S of sorts (or types), X of variables, F of function symbols, and a function assign : X ∪ F → S + , a many-sorted first-order language L is a collection of these objects represented as a tuple L = S, X , F, assign

The function assign assigns sorts to symbols. The sort of a variable x in X is a tuple of one element from S. The sort of a function symbol f in F is a tuple of n + 1 elements from S, with n ∈ N being called the arity of f , which is referred to as an n-ary symbol. Nullary, i.e. 0-ary, functions are called constants.

• Definition 2.2 (Terms). Given a language L and a sort τ ∈ S, the sets of τ -terms are the least sets, according to the inclusion order, defined inductively as follows:

(i) a variable x of sort τ is a τ -term;

(ii) if f is an n-ary function symbol of sort τ 1 , . . . , τ n , τ and t 1 , . . . , t n are τ 1 -, . . . , τ nterms, respectively, then

f (t 1 , . . . , t n ) is a τ -term.
The set of all τ -terms is denoted as T τ . Every τ -term is a term. The set of all terms is

T = τ ∈S T τ . •
Variables of sort τ are also referred to as τ -variables. A τ -term f (t 1 , . . . , t n ) is also referred to as an application or f -application over the parameters t 1 , . . . , t n , with f being the top symbol of the application. Whenever convenient and unambiguous, we drop the τ from our denomination.

A constant is a ground term. A term f (t 1 , . . . , t n ) is ground if and only if t 1 , . . . , t n are all ground -ground terms are those without variables. The subterm relation is defined recursively as follows: a term is subterm of itself; if a term is an application, all subterms of its parameters are also its subterms.

In order do build formulas, we assume that the language contains logical symbols: a Bool ∈ S sort; a family ( : τ, τ, Bool ) τ ∈S of equality symbols, the connectives ¬ (negation) and ∨ (disjunction), and the binder ∀ (universal quantification). We refer to equality over Bool as equivalence. Nullary function symbols of sort Bool are called propositions.

Definition 2.3 (Formulas). Given a language L , the set of L -formulas is the least set defined inductively as follows:

(i) if t 1 and t 2 are τ -terms, for some sort τ , then t 1 t 2 is a formula;

(ii) if p is an n-ary function symbol of sort τ 1 , . . . , τ n , Bool and t 1 , . . . , t n are τ 1 -, . . . , τ nterms, respectively, then p(t 1 , . . . , t n ) is a formula;

(iii) if ϕ is a formula, ¬ϕ is a formula;

(iv) if ϕ 1 and ϕ 2 are formulas, then ϕ 1 ∨ ϕ 2 is a formula;

(v) if x is a variable and ϕ is a formula, then ∀x. ϕ is a formula.

•

Formulas are therefore terms of type Bool. A formula ∀x. ϕ is called a quantified formula, with ϕ being its body and x a bound variable. Formulas t 1 t 2 and p(t 1 , . . . , t n ) are atomic formulas, or atoms. A literal is either an atom or its negation. Given a sort τ , the set of all τ -terms in a formula ϕ is T τ (ϕ), and the set of all terms in a formula ϕ is

T(ϕ) = τ ∈S T τ (ϕ).
The following conventions are adopted in the rest of this thesis:

t 1 t 2 def = ¬(t 1 t 2 ) [Disequality] ϕ 1 ∧ ϕ 2 def = ¬(¬ϕ 1 ∨ ¬ϕ 2 ) [Conjunction] ϕ 1 → ϕ 2 def = ¬ϕ 1 ∨ ϕ 2 [Implication] ∃x. ϕ def = ¬∀x. ¬ϕ [Existential Quantification] ∀x 1 . . . x n . ϕ def = ∀x 1 . (∀x 2 . . . . (∀x n . ϕ) . . . ) [Multiple universal quantification]
Definition 2.4 (Free variables). Given an L -formula ϕ, its set of free variables FV(ϕ) is defined 2.1. Syntax recursively as:

FV(x) = {x} FV(f (t 1 , . . . , t n )) = n i=1 FV(t i ) FV(t 1 t 2 ) = FV(t 1 ) ∪ FV(t 2 ) FV(¬ϕ) = FV(ϕ) FV(ϕ 1 ∨ ϕ 2 ) = FV(ϕ 1 ) ∪ FV(ϕ 2 ) FV(∀x. ϕ) = FV(ϕ) \ {x} • A formula ϕ is a sentence, closed formula, if and only if FV(ϕ) = ∅.
A formula is quantifierfree if and only if it does not contain quantifiers, ground if and only if it is a quantifier-free sentence. The set of bound variables of a formula ϕ is denoted BV(ϕ), consisting of the least set defined inductively as the union of the sets of bound variables occurring in subformulas of ϕ.

Definition 2.5 (Substitution). A substitution is a function σ : X → T, such that σ = {x 1 → t 1 , . . . , x n → t n }, with x i = x j , for 1 ≤ i < j ≤ n, n ∈ N + ,
maps each τ -variable x i into a τ -term t i and every other variable not in x 1 , . . . , x n to itself. The domain of σ, written dom(σ), is defined as the set of variables {x 1 , . . . , x n } that σ is replacing by terms that are not themselves, i.e. dom(σ) = {x | x ∈ X and σ(x) = x}, while the range of σ, written ran(σ), is the set of substituted terms, i.e. ran(σ) = {σ(x) | x ∈ dom(σ)}. A substitution σ is ground if and only if every term in ran(σ) is ground.

The application of a substitution is recursively defined over terms as follows:

xσ = σ(x) f (t 1 , . . . , t n )σ = f (t 1 σ, . . . , t n σ) (t 1 t 2 )σ = t 1 σ t 2 σ (¬ϕ)σ = ¬(ϕσ) (ϕ 1 ∨ ϕ 2 )σ = ϕ 1 σ ∨ ϕ 2 σ (∀x. ϕ)σ = (∀z. (ϕ{x → z}))σ, with z being a fresh variable of the appropriate sort, i.e. z ∈ dom(σ) ∪ ran(σ) ∪ FV(σ)
Composition of substitutions σ and ρ, denoted σ • ρ, is defined as for functions (i.e., ρ is applied first). When written in postfix notation, the composition is ρσ. The fixed-point of a substitution σ is a sequence of applications σ = σ . . . σ such that σ σ = σ . A substitution σ is acyclic if and only if, for any variable x, x does not occur in xσ . A formula ψ 1 is an instance of a formula ψ 2 if and only if there is a substitution σ such that ψ 1 = ψ 2 σ. The substitution σ is referred to as an instantiation of ψ 2 .

•

The application of a substitution is both respectful of shadowing, i.e. it does not substitute bound variables, and capture-avoiding: it avoids, by introducing renamings when necessary, to replace variables by terms whose free variables would be "captured" by a quantifier, i.e. become bound by it.

Definition 2.6 (Subformulas and polarity). Given an L -formula ϕ, the sets of subformulas with positive, negative, and both polarities, denote respectively by SF + (ϕ), SF -(ϕ), and SF ± (ϕ), are the least sets such that

(i) ϕ ∈ SF + (ϕ); (ii) if ¬ψ ∈ SF + (ϕ) (resp. SF -(ϕ)); then ψ ∈ SF -(ϕ) (resp. SF + (ϕ)); (iii) if ψ 1 ∨ ψ 2 ∈ SF ± (ϕ), then {ψ 1 , ψ 2 } ⊆ SF ± (ϕ); (iv) if ∀x.ψ ∈ SF ± (ϕ), then ψ ∈ SF ± (ϕ).
The set of subformulas SF(ϕ) is defined as

SF(ϕ) = SF + (ϕ) ∪ SF -(ϕ). • A subformula occurs positively, resp. negatively, in ϕ if and only if it is in SF + (ϕ), resp. in SF -(ϕ).
Definition 2.7 (Skolem Normal Form). An L -formula ϕ is in Skolem form if and only if no quantified subformula ∃x. ψ 1 occurs positively and no quantified subformula ∀x. ψ 2 occurs negatively. In this case, ϕ is referred to as a Skolem formula. • Definition 2.8 (Conjunctive Normal Form). An L -formula ϕ is in conjunctive normal form

(CNF) if it is a conjunction of disjunctions of literals. Therefore a formula in CNF has the form n i=1 C i , in which each C i has the form m j=1 l ij , for literals l ij and n, m ∈ N + . Each C i is denoted a clause.

•

Formulas in CNF will conventionally be written as sets of clauses {C 1 , . . . , C n }, and clauses as sets of literals {l i1 , . . . , l im }, such that whether the set stands for a conjunction or a disjunction of its elements is to be inferred from the context. Sets that stand for a conjunction, respectively for a disjunction, of their elements are said to be conjunctive, respectively disjunctive. Conjunctive or disjunctive sets may be written as conjunctions or disjunctions, respectively, whenever convenient and unambiguous.

We use the notations ān and (a i ) n i=1 to denote the tuple, or vector, (a 1 , . . . , a n ), in which n ∈ N + . We write [n] for {1, . . . , n}.

Semantics

The machinery for the assessment of truth and falsehood for terms in a language L , and therefore meaning to the language, is presented below.

Semantics

Definition 2.9 (Structure). An L -structure A is defined as a pair A = D, I , in which D is a frame, defined as a collection of non-empty domain sets D τ , for each sort τ ∈ S, and I is an interpretation function that maps n-ary function symbols f of sort τ 1 , . . . , τ n , τ to total functions

f I : D τ 1 × • • • × D τn → D τ
The elements of each domain D τ are referred to as domain elements of sort τ . The domain of the sort Bool is the set of truth values { , ⊥}. We say that a structure is finite if and only if all domain sets in its frame are finite. Respectively, a structure is infinite if any of its domain sets are infinite.

• Definition 2.10 (Valuation and Interpretation). Given an L -structure A = D, I , a valuation for A is a function V : X → D, such that each τ -variable x ∈ X is mapped to an element in D τ .

An L -interpretation M comprises a structure A and a valuation V, such that M = A, V .

We say that M is a finite interpretation if and only if A is a finite structure. Respectively, M is an infinite interpretation if and only if A is an infinite structure.

•

Consider valuations V and V and a set of variables Z. V agrees with V except for Z if and only if, for every variable x ∈ Z, V (x) = V(x). V and V agree on Z if and only if

V (y) = V(y),
for every variable y ∈ Z. Definition 2.12 (Evaluation in an interpretation). Given an L -interpretation M = A, V and an L -formula ψ, the evaluation of ψ in M, noted ψ M , is defined recursively as follows: In this thesis we are mainly concerned with a specific kind of interpretation: as defined in Baumgartner and Waldmann [START_REF] Baumgartner | Hierarchic Superposition with Weak Abstraction[END_REF], an L -interpretation M is term-generated if and only if every element in a domain set D τ is the interpretation of some ground τ -term. These are the type of interpretations we are going to build when automatically assessing satisfiability of formulas. Due to the Herbrand theorem, we know that checking satisfiability of closed Skolem formulas in many-sorted first-order logic with equality can be reduced to checking satisfiability of ground instances. Therefore it suffices to look for term-generated models when trying to assess satisfiability.

x M = V(x) f (t 1 , . . . , t n ) M = f I ( t 1 M , . . . , t n M ) t 1 t 2 M = if and only if t 1 M = t 2 M ; ⊥ otherwise ¬ϕ M = if and only if ϕ M = ⊥; ⊥ otherwise ϕ 1 ∨ ϕ 2 M = if and only if ϕ 1 M = or ϕ 2 M = ; ⊥ otherwise ∀x. ϕ M = if
Next we define the more general problem that our work addresses: that of determining satisfiability when considering theories. In general not only one but a combination, i.e. a union, of theories is considered when checking satisfiability. We follow Barrett et al. [START_REF] Barrett | Satisfiability Modulo Theories[END_REF] for establishing satisfiability modulo a combination of theories defined through classes of interpretations. We assume that if the theories were defined axiomatically, as in Definition 2.14, their combination could be made simply by the union of their axioms (if the languages were disjoint, otherwise through a renaming of common symbols that takes into account whether shared function symbols are meant to stand for the same function). Consider theories T 1 = Th(Ω 1 ) and

T 2 = Th(Ω 2 ), in which Ω 1 is a class of L 1 -interpretations
and Ω 2 a class of L 2 -interpretations, with L 1 and L 2 being disjoint. Assume that both Ω 1 and Ω 2 are closed under isomorphisms. The combination T 1 ⊕T 2 is defined by the class Ω 1+2 of (L 1 ∪L 2 )interpretations such that, for every interpretation in Ω 1+2 , its L 1 -reduct is an interpretation in Ω 1 and its L 2 -reduct is an interpretation in Ω 2 . This way, determining satisfiability modulo

T = T 1 ⊕ T 2 to an L -formula ϕ, with L ⊇ (L 1 ∪ L 2 )
, amounts, as before, to finding an L -model M for ϕ which extends Ω 1+2 .

•

Chapter 3

Satisfiability modulo theories solving

We have formally defined the problem of satisfiability modulo background theories in manysorted first-order logic with equality. We now proceed to the main topic of this thesis: how to automatically determine the satisfiability of a first-order formula while taking into account a set of theories. This is commonly known as the SMT problem. Its relevance comes from the considerable gain in expressivity achieved by combining first-order logic with theories. Reasoning efficiently in such a setting is of utmost importance to a variety of formal methods applications that can rely on logic to encode problems. This allows computer-aided reasoning to be applied on e.g. formal verification, program synthesis, automatic testing, program analysis, and so on.

The focus on real-world problems imposes a restriction on the relevant solutions to a given SMT problem. One generally is interested only in solutions which are extensions of the standard models of the background theories. So in practice, when solving e.g. a satisfiability problem modulo linear integer arithmetic, the only desired solutions are those that interpret the symbols +, -, <, and so on, in the usual way over the integer domain. One benefit of fixing interpretations for theories, rather than relying e.g. on axiomatizations, is to be able to use ad-hoc (decision)

procedures for these specific structures, instead of relying on general purpose methods. For combinations of quantifier-free theories this often leads to highly efficient decision procedures.

The importance of the SMT problem led to the field of research commonly know as "SMT solving" (see [START_REF] Sebastiani | Lazy Satisability Modulo Theories[END_REF] or [START_REF] Barrett | Satisfiability Modulo Theories[END_REF] and Shostak [START_REF] Shostak | Deciding Combinations of Theories[END_REF]. The focus has been generally on quantifier-free logics, which are often decidable. Modern approaches started in the late 1990s, harnessing the power of SAT solvers to build more scalable systems. These approaches can be classified in two broad classes. In the first,

an SMT problem is fully encoded into a SAT instance and fed into a SAT solver, without further intervention. Theory reasoning is performed only in order to provide a better encoding into SAT. In the second, the theory reasoning is performed by a combination of decision procedures that are interleaved with a SAT solver. The SMT problem is abstracted as a SAT instance, whose solution is only a candidate one for the original problem: a propositionally consistent conjunction of literals, which is then checked for consistency modulo the respective theories.

The CDCL(T ) framework [START_REF] Nieuwenhuis | Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)[END_REF] is such an approach for SMT solving. It is the most common one adopted for systems performing automatic SMT solving. Our focus is in this framework and, more importantly, on how to reason efficiently with quantified formulas on it.

In classical logics, the dual problem of satisfiability is that of theorem proving: showing that a formula is a theorem is equivalent to showing that its negation is unsatisfiable, while finding a model for its negation provides a counter-example to the conjecture. The field of automatic theorem proving (ATP) historically was focused on pure and equational first-order logic, where the biggest challenge is how to efficiently handle quantified formulas. Theory reasoning in the presence of quantifiers poses steep challenges, as it is often incomplete and hard to be performed efficiently even in an heuristic manner. Nevertheless, numerous works have tried to extend ATP systems with theory reasoning, to the point that the differences between SMT solvers and ATP systems are becoming increasingly smaller.

CDCL(T ) framework

As previously described, what is commonly known as an SMT solver is a system implementing the CDCL(T ) calculus, by Nieuwenhuis et al. [START_REF] Nieuwenhuis | Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)[END_REF]. Examples of such systems are the widely used CVC4 [START_REF] Barrett | CVC4[END_REF] and Z3 [START_REF] Mendonça De Moura | Z3: An Efficient SMT Solver[END_REF] solvers, as well as Yices [START_REF] Dutertre | Yices 2.2[END_REF] and veriT [START_REF] Bouton | veriT: An Open, Trustable and Efficient SMT-Solver[END_REF].

CDCL(T ) is an extension to the conflict-driven clause learning (CDCL) calculus that accommodates theory reasoning. CDCL is a refinement of the classic DPLL [START_REF] Davis | A Machine Program for Theorem-proving[END_REF] procedure that combines a backtracking search for a propositional model with a powerful conflict analysis engine. The search is performed by interleaving "decisions", i.e. heuristic assignments of literals, with the application of unit propagation until a fixpoint. The explicit backtracking is performed by means of a learned clause derived when a conflict is reached in the search.

Considering a theory T , which is generally a combination of theories T 1 , . . . , T n , such as the theory of equality and uninterpreted functions 1 and linear arithmetic, CDCL(T ) determines the satisfiability of a first-order formula ϕ, in conjunctive normal form (CNF), modulo the theory T . Here we assume that ϕ is quantifier-free. How to handle quantified formulas in a CDCL(T ) architecture is discussed in the next section. The reasoning modulo each theory T i is performed by a specific theory solver, which is generally a decision procedure for the T i -satisfiability of a conjunction of literals in the language of T i . Even though theory solvers cannot be combined modularly in general -there are theories whose satisfiability problem is decidable in isolation but not when combined with other theories -some restricted scenarios allow successful combinations. The Nelson-Oppen framework [START_REF] Nelson | Simplification by Cooperating Decision Procedures[END_REF] is a common choice for combining theory solvers into a decision procedure for the overall combination. It does not impose too many formal restrictions on the considered theories and can lead to efficient implementations. With such a framework, from models obtained by each theory solver a model for the combination of the theories can be built, if it exists. The procedure in Figure 3.1 summarises how the calculus is applied. The Process routine normalises the input formula into CNF and performs transformations aiming to optimise the solving. Examples of such transformations are arithmetic simplifications and applying symmetry breaking [START_REF] Déharbe | Exploiting Symmetry in SMT Problems[END_REF]. The result of Process must be equisatisfiable to the input formula, i.e. if the original formula had a model extending the intended model of T , so will the processed formula, and vice-versa. Generally, a SAT solver implementing CDCL embodies CheckBoolean. Its input is the propositional abstraction of the formula, obtained with the function abs. It maps every distinct atom into a distinct proposition. If the formula is propositionally satisfiable, the SAT solver outputs a conjunction of propositions, commonly known as an assignment, representing a valuation that makes abs(ϕ) true: the found assignment entails the propositional abstraction of the input formula. The set of literals whose abstractions appear in the assignment is represented by E. If E is empty, the formula is propositionally unsatisfiable, therefore it is also T -unsatisfiable. Since by construction the satisfiability of E entails the satisfiability of ϕ, every model of E is also a model for ϕ. From now on we will ambiguously refer to E as a candidate model for the original formula, due to the entailment relationship between them.

function CheckSat(ϕ, T ) is ϕ ← Process(ϕ) // Simplifications, CNF transformation do E ← CheckBoolean(abs(ϕ)) // SAT solver if E = ∅ then return Unsat C ← CheckGround(E, T ) // Theory solvers ϕ ← ϕ ∪ C while C = ∅ return Sat
The CheckGround module is generally implemented as a combination of specialised solvers for each theory in a Nelson-Oppen framework. Thus it amounts to a ground decision procedure for checking the T -satisfiability of E. If E is T -unsatisfiable, a conflict clause is produced, embodying the explanation for the unsatisfiability of E. This clause is then learned, i.e. it is added to the original problem in order to prevent the SAT solver from deriving again this faulty assignment. If no conflict clause is derived, then E is T -satisfiable, and so is the original formula.

Example 3.1. Let ϕ be the formula

ϕ = a ≤ b ∧ b ≤ a + x ∧ x 0 ∧ [f (a) f (b) ∨ (q(a) ∧ ¬q(b + x))]
We evaluate the satisfiability of ϕ modulo the combination T of the quantifier-free theories of equality and uninterpreted functions and linear real arithmetic. This combination is decidable.

The processing of ϕ yields the CNF

ϕ = a ≤ b ∧ b ≤ a + x ∧ x 0 ∧ [f (a) f (b) ∨ q(a)] ∧ [f (a) f (b) ∨ ¬q(b + x)]
whose propositional abstraction is

abs(ϕ) = p a≤b ∧ p b≤a+x ∧ p x 0 ∧ (¬p f (a) f (b) ∨ p q(a) ) ∧ (¬p f (a) f (b) ∨ ¬p q(b+x) )
A satisfying assignment for abs(ϕ) produced by CheckBoolean may be

{p a≤b , p b≤a+x , p x 0 , ¬p f (a) f (b) }
¬(a ≤ b) ∨ ¬(b ≤ a + x) ∨ ¬(x 0) ∨ f (a) f (b)
is derived and added to ϕ. After another iteration of the loop, a candidate model for the new formula is

E = {a ≤ b, b ≤ a + x, x 0, q(a), ¬q(b + x)}
which is also unsatisfiable in this combination of theories. By adding the conflict clause

¬(a ≤ b) ∨ ¬(b ≤ a + x) ∨ ¬(x 0) ∨ ¬q(a) ∨ q(b + x)
to the new formula the SAT solver will be unable to produce a satisfying assignment. Therefore the procedure halts and answers Unsat, showing that the original formula ϕ is T -unsatisfiable.

The key element in the quantifier-free CDCL(T ) architecture are the theory solvers. They are generally ad hoc, with specialised (decision) procedures tailored to the theory in question.

An important element in the use of these solvers is whether they are invoked offline or online2 .

Invocations are done online when they occur at every decision point in the SAT solver search: after a decision is made and the SAT solver propagates until saturation, the theory solver is invoked to analyze the current assignment. An offline invocation occurs only when the SAT solver has provided a model for the propositional abstraction of the formula, i.e. a full assignment. For simplicity, in Figure 3.1 it is assumed that theory solvers are called offline. In practice, however, they are generally employed online. This allows for propositional assignments to be discarded as soon as they become T -unsatisfiable, thus avoiding the consideration of all full assignments extending the refuted one.

Another point for theory solvers is that they generally enjoy some important features (as described in [START_REF] Sebastiani | Lazy Satisability Modulo Theories[END_REF] and [START_REF] Barrett | Satisfiability Modulo Theories[END_REF]) to make the most of the CDCL(T ) framework:

-Model generation: when the procedure witnesses the consistency of the set of literals in its theory, it is capable of producing a model and communicating it to the other components of the framework.

-Conflict set generation: when the procedure attests the inconsistency of the set of literals in its theory, it produces a (possibly minimal) subset from the given set of literals which explains its unsatisfiability.

-Incrementality and backtrackability: the theory solver is stateful between different calls from the outer loop. When checking an assignment, only literals not previously asserted are evaluated. This can lead to significant performance gains, considering that theory solvers may be called numerous times while the SAT solver derives candidate models. This is specially the case when an online approach is implemented, with calls occurring at each partial propositional assignment.

-Propagation: the solver is capable of propagating useful information (such as asserting literals previously undefined in the SAT solver assignment) from the current candidate model. This often leads to significant reductions of the potential search space by deriving useful constraints.

Quantified formulas in CDCL(T )

Reasoning with quantifiers modulo background theories is often costly and not decidable in general. Historically, in the CDCL(T ) framework mainly heuristic instantiation techniques have been used to tackle this problem. They allow to quickly derive ground instances from quantifiers and turn the reasoning back to the efficient ground solver. Here we describe the main instantiation techniques applied in CDCL(T ). Inst, which embodies a quantifier module. The satisfiability check is subsequently performed in the processed formula augmented with the generated instances.

function CheckSatQ(ϕ, T ) is ϕ ← Process(ϕ) // Simplifications, CNF transformation do E, Q ← CheckBoolean(absQ(ϕ)) // SAT solver if E ∪ Q = ∅ then return Unsat C ← CheckGround(E, T ) // Theory solvers if C = ∅ then ϕ ← ϕ ∪ C continue I ← Inst(E, Q, T ) //
The set I is composed of instantiation lemmas ∀x n . ψ → ψσ from the quantified formulas ∀x n . ψ in Q, in which ψσ is a ground instance. When Inst does not lead to an overall refutational complete procedure, there is no guarantee that if the original formula is unsatisfiable then ground T -unsatisfiability will be derived through instantiation.

Similarly, when no instances are generated, the overall procedure can only answer Sat if the instantiation module is such that models can be produced when no more instances can be derived.

If these conditions are not met, CheckSatQ may loop indefinitely or answer Unknown. Below we overview in detail the main general purpose techniques for implementing an instantiation module.

Trigger based instantiation

The most common instantiation technique in SMT solving is based on the following observation [START_REF] Gregory | Techniques for Program Verification[END_REF]: while a quantified formula ∀x n . ψ is semantically equivalent to the infinite conjunction σ ψσ, in which σ ranges over all substitutions, only part of these instances are "relevant" to prove that the overall formula is unsatisfiable. Moreover, considering as relevant instances those containing terms appearing in the ground model is an effective trade off between completeness and efficiency.

This set of relevant instances is approximated through a selection of terms occurring in the quantified formula. Instantiations are derived by solving the E -matching of these selected terms with terms occurring in the ground model. Solutions are substitutions that make two terms equal modulo the equalities in E. The resulting instantiations yield ground formulas. These sets of selected terms are called triggers.

Definition 3.1 (E -matching). Given a conjunctive set of equality literals E and terms u and t, with t ground, the E -matching problem is that of finding substitutions σ such that E |= uσ t holds.

Definition 3.2 (Triggers). A trigger T for a quantified formula ∀x n . ψ is a set of non-ground

terms u 1 , . . . , u m ∈ T(ψ) such that {x n } ⊆ FV(u 1 ) ∪ • • • ∪ FV(u m ).
I = m i=1 ∀x n . ψ → ψσ T i = {u 1 , . . . , u m i }, E |= u 1 σ t 1 , . . . , E |= u m i σ t m i ,
in which t 1 , . . . , t m i are ground terms from E 3. adding the lemmas in I to the original problem Instantiations are determined by computing substitutions for the variables in the selected terms. These substitutions are the solutions for the simultaneous E -matching problem of the selected terms and chosen ground terms occurring in E. Solutions are substitutions for which E groundly entails that each selected term is equal, modulo the theory of equality, to the respective ground term.

An abstract version of the algorithm to compute such substitutions, as presented by de Moura and Bjørner [START_REF] De | Efficient E-Matching for SMT Solvers[END_REF], is

ematch(x, t, S) = {σ ∪ {x → t} | σ ∈ S, x ∈ dom(σ)} ∪ {σ | σ ∈ S, E |= xσ t} ematch(t , t, S) = S if E |= t t ∅ otherwise ematch(f (s n ), t, S) = f ( tn) ∈ T(E), E|=f ( tn) t
ematch(s n , t n , . . . , ematch(s 1 , t 1 , S) . . . ) in which x is a variable, t is a ground term, s is a term, and S is a set of substitutions. All instantiations for a quantified formula with a trigger T = {u 1 , . . . , u n } can be obtained with the set of substitutions S = t 1 , ..., tn∈T(E) ematch(u n , t n , . . . , ematch(u 1 , t 1 , {σ}) . . . ) in which σ is a substitution mapping the variables in T to themselves.

Even though E -matching is an NP-complete problem, it can be performed efficiently in the context of a CDCL(T ) solver (see e.g. [START_REF] De | Efficient E-Matching for SMT Solvers[END_REF] describing an implementation in the Z3 solver).

Implementations exploit the E -graph that is generally maintained by the ground solver. This data structure is a concretization of the separation of the set of terms T(E) into congruence classes according to the congruence relation . There is no standard trigger selection strategy, but recent work by Leino and Pit-Claudel [START_REF] K. Rustan | Trigger Selection Strategies to Stabilize Program Verifiers[END_REF] combines typical approaches and introduces some sophisticated criteria. A possible strategy to be extracted from their work is as follows:

1. Traverse a quantified formula and annotate terms as trigger heads or trigger killers. 3. The remaining candidates are ordered by specificity. Let T 1 , T 2 be candidate triggers. T 1 is less specific than T 2 if and only if all matchings of T 2 are also matchings for T 1 . This is the case when for each trigger head t in T 1 there is a trigger head t in T 2 such that t matches t , i.e. there is a substitution σ such that tσ = t . 4. Finally, the possible triggers for the quantified formula are the minimal candidates.

Example 3.3. Consider again the quantified formula ∀x. f (x) g(h(x)). The possible triggers derived with the above strategy would be only T 1 = {f (x)} and T 2 = {h(x)}, since any trigger with g(h(x)) will be less specific than T 2 and any non-singleton trigger will not be parsimonious.

Avoiding matching loops A matching loop occurs when quantifiers generate instances that only serve to re-instantiate them, thus locking the solver in an infinite chain of instantiations.

Example 3.4 ([Rey16]

). Consider the formula ∀x. f (f (x)) f (x) with the trigger T = {f (x)}.

An instantiation {x → t} will add the term f (f (t)) to the problem, which will subsequently lead to a possible new instantiation {x → f (t)} for this trigger, which would generate a term

f (f (f (t))
) and so on.

Up to now solutions have been proposed only to the cases in which loops depend on a single quantifier, i.e. when the instances of a quantifier directly trigger new instantiations of the same formula. Leino and Pit-Claudel [START_REF] K. Rustan | Trigger Selection Strategies to Stabilize Program Verifiers[END_REF] propose selection strategies to avoid matching loops. In the above example the trigger {f (x)} would be discarded because it is a subterm of a term in the same formula, namely f (f (x)). The only possible trigger for this formula would be {f (f (x))}, which would not lead to looping instantiations on this quantifier. Other works rely not on trigger selection strategies, but on the handling of produced instances. Ge et al. [START_REF] Ge | Solving Quantified Verification Conditions Using Satisfiability Modulo Theories[END_REF] consider instantiations in a breadth-first manner by associating levels to instantiated terms, while de Moura and Bjørner [START_REF] De | Efficient E-Matching for SMT Solvers[END_REF] and Barbosa [Bar16] discard instances based on their activity, measured according to the participation of instances in conflicts in the SAT solver. All these strategies have shortcomings, given the trade-off between avoiding matching loops and missing relevant instances.

Avoiding explosion

The main issue of trigger based instantiation is the large number of produced instances, which often allow only a few rounds of instantiation before the ground solver is unable to continue the solving.

Example 3.5. Consider the quantified formula ∀xyz.f (x) f (z) → g(y) h(z) and the trigger T = {f (x), g(y), h(z)}. If E contains 100 applications of each function symbol f , g, and h, a million instances will be generated from this trigger for this formula.

Reynolds [START_REF] Reynolds | Conflicts, Models and Heuristics for Quantifier Instantiation in SMT[END_REF] applies a strategy in the CVC4 solver that limits the number of possible instantiations for each trigger, with no more than one term per congruence class being used to generate instances. While their trigger based instantiation is very effective, the problem of generating too many instances remains. Leino et al. [START_REF] Rustan | A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover[END_REF] and later Moskal and Łopuszański [START_REF] Moskal | Fast Quantifier Reasoning With Lazy Proof Explication[END_REF] have used a two-tier approach: the instances, together with the current ground model E, are fed into a secondary SMT solver; after unsatisfiability is (hopefully) attained for this combination, only the instances that were relevant for deriving the conflict are added to the original problem. While this technique is promising, it has not been implemented in state-ofthe-art CDCL(T ) solvers. The approaches for discarding instances in [START_REF] De | Efficient E-Matching for SMT Solvers[END_REF] and [START_REF] Barbosa | Efficient Instantiation Techniques in SMT (Work In Progress)[END_REF] also aim to minimise the number of instances to consider, but their effectiveness is not yet clear.

Conflict based instantiation

The lack of a goal in trigger based instantiation (such as e.g. refuting the candidate model) leads to the production of many instances irrelevant for the solving. Furthermore, unlike other non- Given a candidate model E ∪ Q, an instance ψ is said to be conflicting with

E if E ∧ψ |= T ⊥,
or, alternatively, if E |= T ¬ψ. Therefore, given some quantified formula ∀x n . ψ in Q, finding conflicting instances amounts to searching for a ground substitution σ such that E |= T ¬ψσ.

Adding ∀x n . ψ → ψσ to the original problem will prevent the derivation of that same candidate model. This way all instances produced by conflict based instantiation will a priori be relevant for the solving, witnessing a faulty assignment produced by the SAT solver and preventing its repetition, the same way that learned conflict clauses at the ground and propositional level do. the first instance conflicting with E. However, E |= f (c) g(h(c)), therefore the second instance is not conflicting. Note that the second lemma introduces a literal with the new terms h(c) and g(h(c)), which did not previously appear in E, and whose relevance for the solving is a priori unknown.

Finding conflicting instances Intuitively, the problem of finding conflicting instances for a given quantified formula ∀x n . ψ is much harder than instantiation based on E -matching and triggers. One must check that there is a substitution which makes the negation of ψ to be entailed by E, which can be arbitrarily complicated depending on the literals of ψ and the size of E. Reynolds et al. provide an algorithm to successively turn ψ into a set of matching constraints from which they eventually extract substitutions leading to conflicting instances. It has been implemented in CVC4 and is used as a preliminary phase for trigger based instantiation: the latter is invoked only when the former fails to produce conflicting instances. This led to a significant increase in the number of problems solved by the solver, while generally notably reducing the number of necessary instances to do so. Propagating equalities A very interesting feature of the search for conflicting instances is that as a by-product it might propagate equalities over the terms of E, a desirable feature common in theory solvers in a CDCL(T ) framework. Sometimes when conflicting instances are not found, the constraints produced during the search are equalities among terms in E.

Generating instantiation lemmas based on these constraints will not refute the model, but will potentially reduce the search space. CVC4 also benefits from this technique in their instantiation module. However, finding it requires efficiently checking that E |= T f (a) g(a), which is not derivable by equality reasoning only.

Another limitation is that quantified formulas are each considered independently. This means that there are instances from Q which in combination are conflicting with E but that cannot be found with this technique.

Example 3.10. Let E = {p(a)} and Q = {∀x. q(x), ∀yz. ¬q(y) ∨ ¬p(z)}. There are no substitutions σ, ρ such that E |= ¬q(x)σ or E |= q(y)ρ ∧ p(z)ρ, even though E ∪ Q is clearly inconsistent.

Model based instantiation

([GdM09]). Let E ∪ Q be such that E = {f (a) 0, f (b) 1, a < 2} and Q = {∀x. ¬(5 ≤ x) ∨ f (x) < 0}.
A candidate model M which satisfies E could provide the following interpretations for a, b, and

f a M = 0 b M = 2 f M = λx. ite(x < 2, 0, ite(x < 5, 1, -1))
since f (a) M = 0, f (b) M = 1, and a M < 2. To check whether the interpretation M satisfies ∀x. ¬(5 ≤ x) ∨ f (x) < 0 we consider the dual problem: is there a substitution σ such that (x > 5 ∧ f (x) ≥ 0)σ M holds? Consider an arbitrary substitution σ, with xσ being a term t.

To satisfy the first conjunct t M must be greater than 5, therefore f (t) M must result in -1, since the conditions to the two if-then-else expressions in f M will fail. Thus it is not possible to have a substitution σ to which (x > 5 ∧ f (x) ≥ 0)σ M holds. Indeed M satisfies the quantified formula and therefore is a model for E ∪ Q.

The central challenges in MBQI are building the candidate interpretation and evaluating if it satisfies Q. Ge and de Moura built candidates as above, using lambda and if-then-else expressions to create interpretations for function symbols. These interpretations coincide with the term-generated interpretations from E on known terms and map all other terms to given default values. The evaluation of Q in M is done by using a secondary ground CDCL(T ) solver.

For each quantified formula ∀x n . ψ ∈ Q, the variables xn are replaced by fresh constants kn , and then ¬ψ[ kn ] M is encoded into a ground formula and the secondary ground solver checks its satisfiability. If it is unsatisfiable then ∀x n . ψ M holds, otherwise the interpretations of kn are used to derive a refining instantiation lemma.

Reynolds et al. [RTG+13] introduced alternative methods for constructing and checking

Other frameworks candidate interpretations. While their model construction is in theory similar to the technique by

Ge and de Moura, their way of checking candidates is quite different. By representing candidates with a special data structure, they apply a "bottom-up" approach: an instantiation is picked for the variables of the quantified formula and an efficient evaluation engine determines whether the instantiation leads to the formula being interpreted as ⊥, which would trigger a refining instantiation. This flavour of MBQI is combined by Reynolds et al. [START_REF] Reynolds | Finite Model Finding in SMT[END_REF] with a model minimisation technique for E and the insertion of cardinality constraints in the solving in order to perform finite-model finding.

Other frameworks

Model Construction Satisfiability Calculus The Model-Constructing Satisfiability Calculus (mcSAT) is, analogously to CDCL(T ), a generalization of CDCL that accommodates reasoning modulo theories. It was proposed by de Moura and Jovanović [START_REF] Mendonça De Moura | A Model-Constructing Satisfiability Calculus[END_REF] and has been successfully applied for solving quantifier-free problems with non-linear arithmetic [START_REF] Jovanović | Solving Non-linear Arithmetic[END_REF] and problems with bit-vectors [START_REF] Zeljic | Deciding Bit-Vector Formulas with mcSAT[END_REF]. Differently from CDCL(T ), in mcSAT the conflict-driven learning is performed not only at the propositional level but also at the theory level. The calculus incorporates theory decisions, i.e. heuristic assignments are made also for non-propositional variables, and therefore also the corresponding propagations and explanations of conflicts for the derivation of learned clauses at the theory level. How to incorporate first-order reasoning in the framework is yet to be explored.

Hierarchic Superposition

The superposition [BG94, NR01] calculus is a powerful combination of first-order resolution with orderings and rewriting for equality reasoning. For many years it has been the go-to approach for automatic theorem proving in equational first-order logic.

Performing theory reasoning, however, was not commonly associated with superposition-based systems despite the existence of a number of techniques for integrating it, as SMT solvers were generally more suitable to handle problems with theory symbols.

A prominent approach for handling theories efficiently in superposition is to extend the set of inference rules for abstracting away the theory reasoning, generating ground constraints to be later discharged. An off-the-shelf SMT solver, for instance, can be invoked to evaluate the constraints. This way the theory part of the problem is kept separated from the rest. This technique is called Hierarchic Superposition and was proposed by Bachmair et al. [START_REF] Bachmair | Refutational theorem proving for hierarchic first-order theories[END_REF] and later augmented by Baumgartner and Waldmann [START_REF] Baumgartner | Hierarchic Superposition with Weak Abstraction[END_REF]. Refutational completeness is guaranteed in certain restricted fragments, but nevertheless it has been implemented successfully in the SPASS [AKW09, EKK+11] and Beagle [START_REF] Baumgartner | Beagle -A Hierarchic Superposition Theorem Prover[END_REF] theorem provers to integrate arithmetic reasoning into superposition.

AVATAR modulo theories

The AVATAR architecture proposed by Voronkov [START_REF] Voronkov | AVATAR: The Architecture for First-Order Theorem Provers[END_REF] tightly integrates a superposition theorem prover with a SAT solver in a layered approach. Similarly to the CDCL(T ) framework, the first-order problem is abstracted into a propositional one, with the SAT solver enumerating propositional assignments to be checked at the first-order level by a superposition engine. By employing an SMT solver instead of a SAT solver Reger et al. [START_REF] Reger | AVATAR Modulo Theories[END_REF] extended the approach so that at the first-order level only assignments which are groundly satisfiable, modulo the fixed theories, are considered.

The architecture is implemented in the Vampire [KV13] theorem prover, using the Z3 SMT solver to check ground satisfiability. Moreover, the Vampire theorem prover is also capable of performing theory reasoning directly at the first-order level, by introducing theory axioms into the problem. These are generally quite explosive, but powerful heuristics are used so that the overall system performs well in problems containing linear and non-linear real and integer arithmetic, extensional arrays and algebraic data types.

Free-variables and theories Rümmer [Rüm08] introduced a constraint sequent calculus for first-order logic modulo linear integer arithmetic. It combines a sequent calculus, based on earlier work by Giese [START_REF] Giese | Incremental Closure of Free Variable Tableaux[END_REF] on free variable tableaux, with quantifier elimination, based on the classic Omega test integer programming algorithm [START_REF] Pugh | The Omega Test: a fast and practical integer programming algorithm for dependence analysis[END_REF], yielding a powerful framework that is complete for first-order logic (without functions but with arbitrary uninterpreted predicates) and a decision procedure for Presburger arithmetic, i.e. quantified linear integer arithmetic, being also effective for their combination.

The final calculus enjoys similarities to CDCL(T ). Among other techniques, such as using ground decision procedures for the ground parts of the problem, Rümmer integrated trigger based instantiation [START_REF] Rümmer | E-Matching with Free Variables[END_REF] as an optimization for his systematic handling of quantifiers. This way the completeness results are independent of trigger selection or other heuristics, which are used to potentially improve performance but do not hurt the formal guarantees of the framework.

The calculus has been successfully implemented in the Princess [Rüm12] theorem prover.

A historical shortcoming of tableaux and sequent based calculi is the handling of equality.

Backeman and Rümmer [START_REF] Backeman | Theorem Proving with Bounded Rigid E-Unification[END_REF] built on the above framework to introduce a novel way to perform efficient equality reasoning in such a framework for equational first-order logic. They introduced the problem of bounded simultaneous rigid E -unification (BREU), a decidable variant of the classic (and undecidable) problem of simultaneous rigid E -unification that is generally inherent to performing equality reasoning in these calculi. Their approach has also been successfully implemented in the Princess system.

Certificates

Most automatic provers that support the TPTP syntax for problems generate proofs in TSTP (Thousands of Solutions for Theorem Provers) format [START_REF] Sutcliffe | Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems[END_REF]. A TSTP proof consists of a list of inferences. TSTP does not mandate any inference system; the meaning of the rules and the granularity of inferences vary across systems. For example, the E prover [START_REF] Schulz | System Description: E 1.8[END_REF] Most SMT solvers can parse the SMT-LIB [START_REF] Barrett | The SMT-LIB Standard: Version 2.5[END_REF] format, but each solver has its own output syntax. Z3's proofs can be quite detailed [START_REF] Mendonça De Moura | Proofs and Refutations, and Z3[END_REF], but rewriting steps often combine many rewrites rules. CVC4's format is an instance of LF [START_REF] Harper | A Framework for Defining Logics[END_REF] with Side Conditions (LFSC) [START_REF] Stump | Proof Checking Technology for Satisfiability Modulo Theories[END_REF];

despite recent progress [HBR+15, KBT+16], neither skolemization nor quantifier instantiation are currently recorded in the proofs. Proof production in Fx7 [START_REF] Moskal | Rocket-Fast Proof Checking for SMT Solvers[END_REF] is based on an inference system whose formula processing fragment is subsumed by ours; for example, skolemization is more ad hoc, and there is no explicit support for rewriting.

Proof assistants for dependent type theory, including Agda, Coq, Lean, and Matita, provide very precise proof terms that can be checked by relatively simple checkers, meeting De Bruijn's criterion [START_REF] Barendregt | The challenge of computer mathematics[END_REF]. Exploiting the Curry-Howard correspondence, a proof term is a λ-term whose type is the proposition it proves; for example, the term λx. x, of type A → A, is a proof that A implies A. Proof terms have also been implemented in Isabelle [START_REF] Berghofer | Proof Terms for Simply Typed Higher Order Logic[END_REF], but they slow down the system considerably and are normally disabled. Frameworks such as LF, LFSC, and Dedukti

[CD07] provide a way to specify inference systems and proof checkers based on proof terms. Our encoding into λ-terms is vaguely reminiscent of LF.

Isabelle and the proof assistants from the HOL family (HOL4, HOL Light, HOL Zero, and ProofPower-HOL) are based on the LCF architecture [START_REF] Michael | Edinburgh LCF: A Mechanised Logic of Computation[END_REF]. Theorems are represented by an abstract data type. A small set of primitive inferences derives new theorems from existing ones. This architecture is also the inspiration behind automatic systems such as Psyche [START_REF] Graham-Lengrand | Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture[END_REF].

In Cambridge LCF, Paulson introduced an idiom, conversions, for expressing rewriting strategies [START_REF] Paulson | A Higher-Order Implementation of Rewriting[END_REF]. A conversion is an ML function from terms t to theorems of the form t u. Basic conversions perform β-reduction and other simple rewriting. Higher-order functions combine conversions. Paulson's conversion library culminates with a function that replaces Edinburgh LCF's monolithic simplifier. Conversions are still in use today in Isabelle and the HOL systems.

They allow a style of programming that focuses on the terms to rewrite-the proofs arise as a side effect. Our framework is related, but we trade programmability for efficiency on very large problems. Remarkably, both Paulson's conversions and our framework emerged as replacements for earlier monolithic systems.

Over the years, there have been many attempts at integrating automatic provers into proof assistants. To reach the highest standards of trustworthiness, some of these bridges translate the proofs found by the automatic provers so that they can be checked by the proof assistant. The Part I

Instantiation

Chapter 4

Congruence closure with free variables

As shown in Section 3.2, a central problem when applying instantiation techniques to handle quantified formulas in the CDCL(T ) framework is how to determine which instances to derive.

Each of the main techniques, be it trigger, conflict or model based instantiation, contributes greatly to the efficiency of state-of-the-art solvers, yet each one is typically implemented independently, in an ad-hoc manner and within their own specific settings.

In this chapter we present a uniform framework for reasoning with quantified formulas in the theory of equality and uninterpreted functions in CDCL(T ). We introduce the E-ground Conventions Throughout the chapter we assume, for simplicity, and without loss of generality, that all atomic formulas are equalities and that the term language is mono-sorted.

E = [s ] E and [t] E = [t ] E .
The entailment relation is extended in the expected manner to allow conjunctions and disjunctions in the right hand side.

E-ground (dis)unification

Solving E-ground (dis)unification amounts to finding substitutions such that literals containing free variables hold in a context of currently asserted ground literals. E-ground (dis)unification is intrinsically related to the classic problem of rigid E -unification and is also NP-complete. The classic problem of rigid E -unification is that of, given a set of equalities E and an equality u v, finding a substitution σ such that uσ vσ follows from Eσ by ground equational reasoning, i.e. such that Eσ |= uσ vσ holds. This problem has been studied extensively in the context of automated theorem proving [Bec98, BS01, DV01], specially for the integration of equality reasoning into tableaux [START_REF] Hähnle | Tableaux and Related Methods[END_REF] and sequent calculi [START_REF] Degtyarev | Equality Reasoning in Sequent-Based Calculi[END_REF] based procedures. The simultaneous version of the problem has to be considered in these cases, in which the same substitution σ must be a solution to E -unification problems

E 1 σ |= u 1 σ v 1 σ, . . . , E n σ |= u n σ v n σ. Simultane-
ous rigid E -unification (SREU, for short) was famously shown to be undecidable by Degtyarev and Voronkov [START_REF] Degtyarev | The Undecidability of Simultaneous Rigid E-Unification[END_REF]. Nevertheless, incomplete unification procedures can be used in such a way that an overall complete first-order calculus may be obtained, as shown by Degtyarev and

Voronkov themselves [START_REF] Degtyarev | What You Always Wanted to Know about Rigid E-Unification[END_REF] and by Giese [START_REF] Giese | A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition[END_REF]. Recently Backeman and Rümmer [START_REF] Backeman | Theorem Proving with Bounded Rigid E-Unification[END_REF] provided a complete first-order calculus based on a restricted case of SREU in which the possible substitutions for variables are bound, yielding a decidable problem that they solve through an encoding into SAT, using an off-the-shelf SAT solver to compute solutions.

We define below a variant of (non-simultaneous) E -unification in which we consider equality literals instead of only equalities and in which E is ground. Moreover, we consider a conjunction of literals in the right hand side.

Definition 4.1 (E-ground (dis)unification). Given two conjunctive sets of equality literals E and L, with E ground, the E-ground (dis)unification problem is that of finding substitutions σ such that E |= Lσ holds.

To show that E-ground (dis)unification is indeed a variant of rigid E -unification we prove below that any problem E |= Lσ can be recast with only equalities in E and a single equality in L:

Lemma 4.1 (Reduction to Rigid E -unification). To find solution substitutions σ for an E-ground (dis)unification problem E |= Lσ can be cast to the problem of finding substitutions σ such that E eq σ |= uσ vσ, in which E eq is a conjunctive set of equalities and u, v are terms.

Proof. First, we can assume that E is closed under entailment w.r.t. disequalities. Indeed, for any set of ground equality literals E, retrieving all the disequalities that it entails can be done polynomially. Let be a constant and f a binary function symbol, both not appearing in

E ∪ L. Each disequality s t in E ∪ L is replaced with f (s, t) ∧ f (t,
E ∧ f (u , v ) ∧ f (v , u ) |= f (uσ, vσ) ∧ f (vσ, uσ) ∧ L
continues to hold, as well as that applying the same process to all other disequalities in E |= Lσ preserves the entailment into the resulting

E eq |= s 1 σ t 1 σ ∧ • • • s n σ t n σ
which, by taking a fresh n-ary function symbol f , can then be transformed into the equivalent and L = {h(x 1 ) h(c), h(x 2 ) g(x 3 ), f (x 1 ) f (x 3 ), x 4 g(x 5 )}. A solution σ for their E-

E eq |= f (s 1 , . . . , s n ) f (t 1 , . . . , t n ). Since E eq contains
ground (dis)unification problem E |= Lσ is σ = {x 1 → a, x 2 → c, x 3 → b, x 4 → g(x 5 )}.

E-ground (dis)unification

The above example shows that x 5 can be mapped to any term; this E-ground (dis)unification problem has infinitely many solutions. We show below how the set of all solutions of a given E-ground (dis)unification can be finitely represented. Without loss of generality, we assume that T(E ∪ L) contains at least one ground term.

Theorem 4.2. Given an E-ground (dis)unification problem, if a substitution σ exists such that E |= Lσ, then there is an acyclic substitution σ such that ran(σ ) ⊆ T(E ∪ L), σ is ground, and E |= Lσ .

Proof. First, we can assume that σ is ground. Indeed, if a non-ground substitution σ is such that E |= σ, then E |= σσ g holds for any ground substitution σ g . For convenience and without loss of generality, assume all terms in L are flat. We introduce for this proof the notations

E σ = {x xσ | x ∈ dom(σ)} and S t = {t | t ∈ T(E ∪ L ∪ E σ ) and E ∪ E σ |= t t },
E ∪ E σ |= x 1 f 1 (. . . , x (2 mod n) , . . . ) ∧ x 1 t
for some ground term t. Thus f 1 (. . . , x (2 mod n) , . . . ) and t = f j (. . . , t , . . . ) are congruent, therefore j = 1 and x (2 mod n) and t should be equal. By successive application of the same reasoning step, there exists some x i and a constant a such that E ∪ E σ |= x i a f i (. . . , x (i+1) mod n , . . . ), which contradicts the fact that only one equality contains x i in E σ .

From now on we only consider solutions σ, for a given E-ground (dis)unification problem

E |= Lσ, such that σ is acyclic, ran(σ) ⊆ T(E ∪ L) and E |= Lσ .
As a corollary of Theorem 4.2, the E-ground (dis)unification problem is in NP: it suffices indeed to guess an acyclic substitution mapping variables to terms in T(E ∪ L) whose fixpoint is a ground substitution and check (polynomially) that it is a solution. The problem is also NP-hard, by reduction of 3-SAT.

Theorem 4.3 (E-ground (dis)unification is NP-complete). Finding solutions for E-ground (dis)unification is NP-complete.

Proof. E-ground (dis)unification is NP since it can be verified, in polynomial time, with a classic congruence closure procedure, for instance, that a substitution σ solves the entailment problem.

The proof of its NP-hardness is done through an encoding of 3-SAT into the entailment.

Let C be a set of 3-clauses containing literals over a set of propositions P. Let , ⊥ be constants and p a unary operator such that, for any proposition, p(p) = and p(¬p) = ⊥. For each clause C ∈ C, let f C be a ternary function. For each proposition p ∈ P, let x p be a variable.

The set of equality literals E ∪ L is built such that

E = C= 1 ∨ 2 ∨ 3 ∈ C f C (p( 1 ), p( 2 ), p( 3 )) p( 1 ) = or p( 2 ) = or p( 3 ) = L = C= 1 ∨ 2 ∨ 3 ∈ C f C (x p 1 , x p 2 , x p 3 ) i = p i or i = ¬p i , i ∈ {1..3}
With this encoding the search for a substitution σ such that E |= Lσ can be seen as determining the satisfiability of C.

Recasting instantiation techniques

We show below how each of the main instantiation techniques used in the CDCL(T ) framework are recast using E-ground (dis)unification. This forms the cornerstone of a framework based on a single solving method to be used in a modular way when handling instantiation techniques in CDCL(T ).

Trigger based instantiation

As discussed in Section 3.

E |= (u 1 y 1 ∧ • • • ∧ u m y m ) σ
with the further restriction that σ is acyclic, ran(σ) ⊆ T(E ∪ L) and σ is ground. This forces each y i to be grounded into a term in T(E), thus enumerating all possibilities for E -matching u i . The desired instantiations are obtained by restricting the found solutions to xn .

Q = {∀x. f (x) g(h(x))}. Triggers from Q are T 1 = {f (x)}, T 2 = {h(x)}, T 3 = {f (x), g(h(x))}
and so on. The instantiations from these triggers are derived from the solutions yielded by for the respective problems: -E |= (f (x) y 1 ∧ g(h(x)) y 2 )σ, by σ = {y 1 → f (a), y 2 → g(b), x → a}, also yielding only the instantiation lemma 4.1.

-E |= (f (x) y)σ,

Conflict based instantiation

As discussed in Section 3.2.2, given a ground model E ∪ Q, a conflicting instance with E for a quantified formula ∀x n . ψ ∈ Q is some ground ψσ such that E |= ¬ψσ.

Model based instantiation (MBQI)

As discussed in Section 3.2.3, the satisfiability of E ∪ Q is assessed by attempting to build a model and checking whether it indeed satisfies both E and Q. The interesting case is the satisfaction of Q. It is determined by independently evaluating each of its quantified formulas in the candidate interpretation. This evaluation is performed in much the same way as the search for conflicting instances described in Section 3.2.2 and revisited above in terms of E-ground (dis)unification. We build on this observation to present below an alternative way of performing MBQI. We extend E and look for conflicting instances between Q and this extension through an entailment check defined in terms of E-ground (dis)unification. This way one can evaluate if every model of the resulting extension E tot is also a model of E ∪ Q and, in the negative case, derive instantiations that refine the construction of E tot . Here we follow the model construction guidelines by Reynolds et al. [START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF].

Calculus

Model construction A distinguished term e τ is associated to each sort τ ∈ S. For each f ∈ F with sort τ 1 , . . . , τ n , τ a default value ξ f is defined such that

ξ f = f (t 1 , . . . , t n ) ∈ T(E) if [t 1 ] = [e τ 1 ], . . . , [t n ] = [e τn ] some t ∈ T(E) otherwise
The extension is built such that all ground terms not occurring in E which might be considered when evaluating Q are present in the congruence closure of E tot , according to the respective default values; and all terms in T(E) not asserted equal are explicitly asserted disequal, i.e.

E tot = E ∪ t 1 ,t 2 ∈ T(E) {t 1 t 2 | E |= t 1 t 2 } ∀xn. ψ∈Q,t∈ T(E) f (s n )σ ξ f σ = {x → t}, f (s n ) ∈ T(ψ) and f (s n )σ is not in the CC of E.
Finding model conflicting instances As above, finding conflicting instances amounts to solving the E-ground (dis)unification problem

E tot |= ¬ψσ, for some ∀x n . ψ ∈ Q Example 4.4. Let E = {f (a) g(b), h(a) b}, Q = {∀x. f (x) g(x)
, ∀xy. ψ} and e = a, with all terms having the same sort. The computed default values of the function symbols are

ξ f = f (a), ξ g = a, ξ h = h(a).
∀x. f (x) g(x) → f (a) g(a)
will prevent the derivation of the candidate model E tot again.

Calculus

The intrinsic relation between E -unification and congruence closure has been investigated by Goubault [Gou93] and Tiwari et al. [START_REF] Tiwari | Rigid E-Unification Revisited[END_REF]. They integrate variations of the classic procedure with first-order rewriting techniques and search for solutions guided by the structure of the terms. We build on these ideas and propose a calculus to find substitutions σ solving an Eground (dis)unification problem E |= Lσ. This calculus, Congruence Closure with Free Variables (CCFV), uses a congruence closure algorithm as a core element to guide the search and build solutions. We share with these related works the belief that the congruence closure algorithms, being very efficient at checking solutions, can also be the core of efficient algorithms to discover them. CCFV however differs from those previous techniques notably, since it handles disequalities and more importantly since the search for solutions is pruned based on the structure of a ground model, which makes it most suitable for a CDCL(T ) context.

The calculus proceeds by building a conjunctive set of equations

E σ such that E ∪ E σ |= L,
in which E σ corresponds to a solution substitution built based on the entailment conditions of the literals in L. These conditions are determined according to the structure of the literals and to the signature classes in E. We restrict ourselves to signature classes rather than congruent classes so that less possibilities for solutions need to be considered, since terms with the same signature are indistinguishable with relation to entailment conditions.

] = [t 2 ] 4. is f (u 1 , . . . , u n ) g(v 1 , . . . , v n ) and a) f = g and E |= u 1 σ v 1 σ, . . . , E |= u n σ v n σ or b) there are ground terms t 1 , t 2 ∈ T(E) such that [t 1 ] = [t 2 ], f (u 1 , . . . , u n )σ ∈ [t 1 ], and
g(v 1 , . . . , v n )σ ∈ [t 2 ]
5. is u v and there are ground terms

t 1 , t 2 ∈ T(E) such that E |= t 1 t 2 , uσ ∈ [t 1 ],
and

vσ ∈ [t 2 ]
Proof. Since is either an equality or a disequality, each term is either a variable or a function application, and a variable either occurs or not in a term, the cases shown are exhaustive for the structure of . For each case we show that if, for some arbitrary substitution σ, E |= σ, then one of the side conditions must hold, and that if any side condition holds, then E |= σ.

Calculus

Case

f (a) f (b) ∧ h(a) h(c) ∧ g(b) h(c) |= (h(x 1 ) h(c) ∧ h(x 2 ) g(x 3 ) ∧ f (x 1 ) f (x 3 ) ∧ x 4 g(x 5 )) σ
This substitution can be built by analyzing the entailment conditions for each of the literals in L and how they can be consistently combined. A conjunctive set of equations E σ from which such a substitution can be derived, i.e. such that E ∪ E σ |= L, is built considering that:

h(x 1 ) h(c): either x 1 c, due to condition (4a), or x 1 a, due to (4b), appears in E σ ;

-h(x 2 ) g(x 3 ): either x 2 c ∧ x 3 b or x 2 a ∧ x 3 b, both due to condition (5), appears in E σ ; -f (x 1 ) f (x 3 ): either x 1 x 3 , due to (4a), or x 1 a ∧ x 3 b or x 1 b ∧ x 3 a, both
due to (4b), must be in E σ ;

x 4 g(x 5 ): due to condition (3a), the literal itself must be in E σ .

A possible solution is thus E σ = {x 1 a, x 2 a, x 3 b, x 4 g(x 5 )}, corresponding to the acyclic substitution σ = {x 1 → a, x 2 → a, x 3 → b, x 4 → g(x 5 )}. Note that, for any ground term To simplify the presentation, the rules do not apply branching directly, but build disjunctions on the right part of the state which later lead to branching. A branch is closed when its constraint is decomposed into either ⊥ or . The latter are branches for which E ∪ E σ |= L holds.

t ∈ T(E ∪ L), σ g = σ ∪ {x 5 → t} is such that ran(σ g ) ⊆ T(E ∪ L),
The set of CCFV derivation rules is presented in Table 4.1. As a convention, t stands for a ground term, x, y for variables, u for non-ground terms, u 1 , . . . , u n for terms such that at least one is non-ground and s, s 1 , . . . , s n for terms in general. Rules are applied top-down, the symmetry of equality being used implicitly. Each rule simplifies the constraint of the right hand side of the state, and as a consequence any derivation strategy is terminating (Theorem 4.5).

When an equality is added to the left hand side of a state E σ E C (rule Assign), the constraint C is normalized with respect to congruence closure to reflect the assignments to variables. That is, all terms in C are representatives of classes in the congruence closure of Example 4.6. The rule Ucomp enumerates the possibilities for which a literal of the form f (u 1 , . . . , u n ) f (s 1 , . . . , s n ) is entailed, which may be due to their arguments being congruent, since both terms have the same top symbol, or by E -matching f -terms occurring in the same signature class of E cc . The generated entailment conditions are that either u 1 s 1 , . . . , u n s n can be entailed or there is a term t ∈ T(E) into which both f (u 1 , . . . , u n ) and f (s 1 , . . . , s n ) can be entailed equal. For the second condition to hold there must be f -terms f (t 1 , . . . , t n ) and f (t 1 , . . . , t n ) in [t] such that u 1 t 1 , . . . , u n t n and s 1 t 1 , . . . , s n t n can be entailed.

E ∪ E σ . We write rep(E σ , x) = some chosen y ∈ [x] Eσ if all terms in [x] Eσ are variables rep(E σ , f (s n )) otherwise, for some f (s n ) ∈ [x] Eσ rep(E σ , f (s 1 , . . . , s n )) = f (s 1 , . . . , s n ) if f (s 1 , . . . , s n ) is ground f (rep(E σ ,
E σ E x s ∧ C Assign if x ∈ FV(s) E σ ∪ {x s} E rep({x s}, C) E σ E x f (ū n ) ∧ C Uvar if x ∈ FV(f (ū n )) E σ E [t]∈E cc , f ( tn)∈[t] (x t ∧ u 1 t 1 ∧ • • • ∧ u n t n ∧ C) E σ E f (ū n ) f (s n ) ∧ C Ucomp E σ E (u 1 s 1 ∧ • • • ∧ u n s n ∧ C) ∨ [t]∈E cc , f ( tn)∈[t], f ( t n )∈[t] u 1 t 1 ∧ • • • ∧ u n t n ∧ s 1 t 1 ∧ • • • ∧ s n t n ∧ C E σ E f (ū n ) g(s m ) ∧ C Ugen if f = g E σ E [t]∈E cc , f ( tn)∈[t], g( t m )∈[t] u 1 t 1 ∧ • • • ∧ u n t n ∧ s 1 t 1 ∧ • • • ∧ s m t m ∧ C E σ E x y ∧ C Dvar E σ E [t], [t ]∈E cc , E|=t t (x t ∧ y t ∧ C) E σ E x f (s n ) ∧ C Dfapp E σ E [t], [t ]∈E cc , E|=t t , f ( t n )∈[t ] (x t ∧ s 1 t 1 ∧ • • • ∧ s n t n ∧ C) E σ E f (ū n ) g(s m ) ∧ C Dgen E σ E [t], [t ]∈E cc , E|=t t , f ( tn)∈[t], g( t m )∈[t ] u 1 t 1 ∧ • • • ∧ u n t n ∧ s 1 t 1 ∧ • • • ∧ s m t m ∧ C E σ E C 1 ∨ C 2 Split E σ E C 1 E σ E C 2 E σ E ∧ C Yield if E |= E σ E C E σ E ∧ C Fail E σ E ⊥ if is ground and E |= Table 4.1: The CCFV calculus in equational FOL. E is fixed from a problem E |= Lσ.
The structural rules (Split, Fail and Yield) create or close branches. Split creates branches when there are disjunctions in the constraint. Fail closes a branch when it is no longer possible to build on the current solution to entail the remaining constraints, i.e. a ground constraint was derived that cannot be entailed by E. Yield removes constraints from the right hand side of the state. When no more constraints remain to be entailed, the empty conjunction is derived. In this case E σ embodies a set of solutions for the given E-ground (dis)unification problem.

Each conjunctive set E σ defines a substitution σ = {x → rep(E σ , x) | x ∈ FV(L)}. If a branch is closed with Yield, the set Sols(E σ ) of all ground solutions extractable from E σ is composed of substitutions σ g which extend σ by mapping all variables in ran(σ ) into ground terms in T(E ∪ L), such that each σ g is acyclic, σ g is ground and E |= Lσ g .

Strategy

A possible derivation strategy for CCFV, given an initial state E L, is to apply the sequence of steps described below at each state E σ E C. Let sel be a function that selects a literal from a conjunction according to some heuristic, such as selecting first literals with less variables or literals whose top symbols have less ground signatures in E cc . The result of sel is denoted selected literal. Since no two rules can be applied on the same literal, the function sel effectively enforces an order on the application of the rules. Moreover, the branch selection strategy assumes that each branch is explored to the end before a new one is considered.

L = {h(x 1 ) h(c), h(x 2 ) g(x 3 ), f (x 1 ) f (x 3 ), x 4 g(x 5
)}, as in Example 4.1. The set of signature classes of E, which coincides with its set of congruence classes, is Let sel select first literals in C with the minimal number of variables. The derivation tree produced by CCFV for this problem is shown below. Selected literals are underlined.

E cc = {{a}, {b}, {c}, {f (a), f (b)}, {h (a), h(c)
Disjunctions and the application of Split are kept implicit to simplify the presentation, as is the handling of x 4 g(x 5 ). Its entailment does not relate with the other literals in L and it can be solved by an early application of Assign.

E h(x 1 ) h(c) ∧ h(x 2 ) g(x 3 ) ∧ f (x 1 ) f (x 3 ) Ucomp A B Since h(x 1 )
h(c) leads to the constraints x 1 c ∨ x 1 a and a subsequent splitting of the derivation, A is

E x 1 c ∧ h(x 2 ) g(x 3 ) ∧ f (x 1 ) f (x 3 ) Assign {x 1 c} E h(x 2 ) g(x 3 ) ∧ f (c) f (x 3 ) Ucomp {x 1 c} E h(x 2 ) g(x 3 ) ∧ x 3 c Assign {x 1 c, x 3 c} E h(x 2 ) g(c) Dgen {x 1 c, x 3 c} E ⊥ Fail {x 1 c, x 3 c} E ⊥ and B is E x 1 a ∧ h(x 2 ) g(x 3 ) ∧ f (x 1 ) f (x 3 ) Assign {x 1 a} E h(x 2 ) g(x 3 ) ∧ f (a) f (x 3 ) Ucomp {x 1 a} E h(x 2 ) g(x 3 ) ∧ x 3 a Assign {x 1 a, x 3 a} E h(x 2 ) g(a) Dgen {x 1 a, x 3 a} E ⊥ Fail {x 1 a, x 3 a} E ⊥ {x 1 a} E h(x 2 ) g(x 3 ) ∧ x 3 b Assign {x 1 a, x 3 b} E h(x 2 ) g(b) Dgen C 1 C 2
with C 1 and C 2 being the following derivations split from the disjunction x 2 a ∨ x 2 c derived from h(x 2 ) g(b):

{x 1 a, x 3 b} E x 2 a Assign {x 1 a, x 2 a, x 3 b} E Yield {x 1 a, x 2 a, x 3 b} E {x 1 a, x 3 b} E x 2 c Assign {x 1 a x 2 c, x 3 b} E Yield {x 1 a, x 2 c, x 3 b} E A solution E σ = {x 1 a, x 2 a, x 3 b, x 4 g(x 5 )} such that E ∪ E σ |= L holds is produced
by C 1 , corresponding to the same E σ respecting the entailment conditions shown in Example 4.5.

Note that C 2 also provides a solution, differing from E σ only on the assignment to x 2 .

Correctness

Theorem 4.5 (Termination). All derivations in CCFV are finite.

Proof. The Split rule is the only one to increase the width of a derivation tree. Its application is bounded by the size of the disjunctions, which in turn is bound by the number of signature classes in E cc . Therefore Split can only be applied a finite number of times. It then suffices to

show that the depth of the tree is also bounded. For simplicity, but without any fundamental effect on the proof, let us assume that all rules but Split are applied on conjunctions. Let Lemma 4.6 (Solutions produce ground substitutions). Given a computed solution E σ for an E-ground (dis)unification problem E |= Lσ, each σ g ∈ Sols(E σ ) is an acyclic substitution such that ran(σ g ) ⊆ T(E ∪ L) and σ g is ground.

Proof. The Assign rule is the only one that augments E σ , adding a term from T(L) to the congruence class of a variable in E cc σ . The occurs check in the side condition, together with the application of rep after the assignment on the remaining constraints in the branch, ensures that a variable is not assigned to a term in which it occurs. Therefore, by induction on the structure of derivation trees, the substitution σ = {x → rep(E σ , x) | x ∈ FV(L)} built from E σ is acyclic and ran(σ) ⊆ T(E ∪ L). Thus each

σ g = x → t rep(Eσ, x) x ∈ FV(L), t rep(Eσ, x) is rep(E σ , x) if rep(E σ , x) is non-variable or some chosen ground t ∈ T(E ∪ L) otherwise
is also acyclic, σ g is ground, and ran(σ g ) ⊆ T(E ∪ L).

Calculus

Lemma 4.7 (Rules capture entailment conditions). There is an applicable rule in the calculus for any arbitrary equality literal .

Proof. If is ground, then Yield or Fail are applicable, according to whether it is entailed by E. We otherwise proceed by case analysis on the structure of the literal, according to the cases in Theorem 4.4.

Case 1, = x y: If x = y, the rule Yield is applicable, otherwise it is Assign.

Case 2, = x f (s 1 , . . . , s n ), and x occurs in f (s 1 , . . . , s n ): The rule Uvar is the only applicable one.

Case 3, = x f (s 1 , . . . , s n ) and x does not occur in f (s 1 , . . . , s n ): the only rule applicable is Assign.

Case 4, = f (u 1 , . . . , u n ) g(v 1 , . . . , v n ): if f = g the rule Ucomp is applied, otherwise
Ugen is.

Case 5, = u v: The rules Dvar, Dfapp, or Dgen are applied depending on the structure of u and v. Since a term is either a variable or a function application, all options are considered.

Lemma 4.8 (Rules preserve entailment conditions). For each rule

E σ E C R E σ E C if there is a ground substitution ρ such that FV(E σ ) ∩ FV(E ρ ) = ∅ and E ∪ E σ ∪ E ρ |= C, then
there is a ground substitution ρ with

FV(E σ ) ∩ FV(E ρ ) = ∅ such that (i) E ∪ E σ ∪ E ρ |= C and (ii) E ∪ E σ ∪ E ρ |= C
Proof. The second condition holds trivially for all rules but Assign, since it is the only one that modifies E σ . We then first analyze Assign for both conditions, starting with the second one.

Let C = C 1 ∧ x s. Therefore E σ = E σ ∪ {x s}.
C is the result of replacing x, and s if it is also a variable, in C 1 by its representative, which is either s or a variable from [x] E σ . Let E ρ be E ρ but without the equality for the variable which disappeared from C 1 in C . Thus, since

E ∪ E σ ∪ E ρ |= C and E σ ∪ E ρ effectively have the same congruence closure as E σ ∪ E ρ , it follows that E ∪ E σ ∪ E ρ |= C.
For the first condition, since C coincides with C 1 but for the replacement of the assigned variable, it also follows from the premise that

E ∪ E σ ∪ E ρ |= C .
We verify the first condition for the remaining rules by case analysis.

Case Split: Due to entailing a disjunction of the considered constraints guaranteeing the entailment of at least one of the disjuncts.

Case Yield: Follows trivially from the properties of conjunction.

Case Uvar: By congruence. Since

x occurs in f (ū n ), E ∪ E σ ∪ E ρ |= x f (ū n )
implies that there are terms t and f ( t n ) in T(E) which are the representatives, in E σ ∪ E ρ , for x and f (ū n ), respectively, such that E |= t f ( tn ) and t occurs in f ( tn ) modulo E. Thus in C there is one disjunct such that

x t ∧ u 1 t 1 ∧ • • • u n t n ∧ C
which is built according to the class [t] E and is trivially entailed by E, since E ∪ E σ ∪ E ρ entailing each of its conjuncts follows from the construction of the disjunct and from the premise.

Proceeding analogously the condition can be shown to also hold for the remaining branching rules.

Theorem 4.9 (Completeness). Let σ be a solution for an E-ground (dis)unification problem

E |= Lσ.
Then there exists a derivation tree starting on ∅ E L with at least one branch closed with Yield such that σ g ∈ Sols(E σ ) and E |= Lσ g .

Proof. Theorem 4.2 ensures that there is an acyclic substitution σ g corresponding to σ such that ran(σ g ) ⊆ T(E ∪ L), σ g is ground and E |= Lσ g . It remains to be shown that CCFV can produce such a substitution. By Lemma 4.7, for any equality literal in L, no matter its shape, a given rule is applicable to assess its entailment. By Lemma 4.8, all rules in CCFV preserve the entailment conditions according to ground substitutions, therefore, by induction on the structure of derivation trees, if there is a solution for L, then there is a branch in the derivation tree starting

from ∅ E L whose leaf is E σ E and σ g ∈ Sols(E σ ) is such that E |= Lσ g .
Theorem 4.10 (Soundness). Whenever a branch is closed with Yield, every

σ g ∈ Sols(E σ ) is such that E |= Lσ g .
Proof. We show by induction on the structure of derivation trees that a resulting ground substitution σ from a branch closed with Yield is indeed a solution for the initial problem at the root. The base case is that at the leaf any substitution σ g ∈ Sols(E σ ) is ground and such that E |= σ * g . Lemma 4.6 ensures that σ g is ground and the entailment holds trivially. Our induction hypothesis is that if the condition holds at the succedent E σ E C of a rule it holds that E |= C σ, then it holds for premise E σ E C that E |= Cσ. We proceed by case analysis, for each rule. Case Uvar: From the premise and by the properties of disjunction, there is at least one disjunct in C σ such that, for some

[t] ∈ E cc and f (t 1 , . . . , t n ) ∈ [t], E |= xσ tσ ∧ u 1 σ t 1 σ ∧ • • • ∧ u n σ t n σ 4.2. Calculus By congruence, E |= f (ū n )σ f ( tn )σ holds. Since we have that E |= t f ( tn ), E |= C σ and Cσ = C σ ∪ {x f (ū n )}σ, it follows that E |= Cσ.
Proceeding analogously the condition can be shown to also hold for the remaining branching rules. Since the induction hypothesis is valid, the condition E |= (C ∧ E σ )σ g also holds at the root, in which C is L and E σ is the empty set. Thus E |= Lσ g .

Corollary 4.11 (CCFV decides E-ground (dis)unification). Any derivation strategy based on the CCFV calculus is a decision procedure for E-ground (dis)unification.

Even though CCFV always finds a solution for an E -ground (dis)unification problem if it has solutions, it only provides the ground solutions σ * such that E |= Lσ * , σ is acyclic and

ran(σ) ⊆ T(E ∪ L).

Instantiating with CCFV

We here show how to use CCFV for computing substitutions for the instantiation techniques cast with E-ground (dis)unification, as described in Section 4.1.1. We also present how CCFV facilitates certain extensions to these techniques.

Trigger based instantiation

The restricted E-ground (dis)unification

E |= (u 1 y 1 ∧ • • • ∧ u n y n ) σ
for a given quantified formula in Q can be solved with CCFV by adding a side condition to

Assign that s must be a ground term and removing the side condition of Uvar. This will lead to the application of Uvar in each u i y i . The desired instantiations are obtained by considering the substitutions extracted from the solutions from branches closed with Yield, ignoring the assignments for ȳn .

Discarding entailed instances Trigger based instantiation may produce instances which are already entailed by the ground model. Such instances most probably will not contribute to the solving, so they should be discarded. Checking this, however, is not straightforward with processing techniques. CCFV, on the other hand, allows it by simply checking, given an instantiation σ for a quantified formula ∀x n . ψ, whether there is a literal ∈ ψ such that solutions in a non-backtracking manner. Sets of solutions may be computed independently and combined according to the dependency between the solved constraints. This way one is not restricted to search only for solutions extending a fixed one.

E ∪ E σ |= , with E σ = {x xσ | x ∈ dom(σ)}.
This new calculus is similar to the previous one, but now a state is an AND-OR combination of solving statements, denoted S. Each solving statement has the form Σ E C, in which Σ is a set of conjunctive equalities representing partial solutions and C, as before, is an AND-OR combination of the remaining constraints to entail. The calculus is shown in Table 4.2. The symbols , and ∧, ∨ are used for writing combinations of solving statements and constraints, respectively. Instead of a derivation tree, the new calculus operates on a single state that is modified in a top-down manner by each rule application. From an initial state { } E L, a fair application of the rules eventually derives either ∅ E ⊥ or Σ E . In the latter case all solutions for the E-ground (dis)unification problem E |= Lσ are contained in Σ. The former case indicates that the problem has no solutions.

The main differences in the calculi come from the structural rules. The branching behave mostly as before. Assign changes only so that now it updates not a single solution but a set of them, keeping the remaining constraints normalised according to all of them. While before disjunctions in the right hand side were abstracted with branching, now the rules explicitly operate on them. Moreover, conjunctions may also be split. The rules Split ∧ and Split ∨ split the search for solutions into simultaneous or orthogonal components, respectively, as represented by the combination of solving statements with or . On the other hand, Meet and Join combine components based on their interdependency. Orthogonal components can be combined only after they have been solved. The rules from Table 4.1 that simplified conjunctive constraints based on entailment from E are extended for simplifying disjunctive constraints. Therefore

Fail ∧ and Yield ∧ coincide with the previous calculus, while Fail ∨ and Yield ∨ apply the dual simplifications for disjunctions. These extended structural rules allow each part of the problem to be solved as independently as desired and the resulting solutions to be later properly combined.

Combining orthogonal solutions, done by Join, is straightforward. It suffices to merge the sets of complete solutions and recover the disjunction in the constraints. The case of simultaneous solutions, however, considers arbitrary constraints and partial solutions and requires closer attention. From two solving statements, Meet generates all possible pairwise combinations of solutions from their respective solution sets. To ensure compatibility, one of the two solutions being combined is chosen and both the remaining constraints and the other solution are normalized according to it. This way if two solutions are not compatible, at least one literal that cannot be entailed will be in the constraints of the generated state. Since the constraints are conjunctive, the faulty statement will eventually be discarded. The normalisation also keeps the invariant that variables which are not their own representatives do not appear in the right hand side of the solving statement.

S Σ E x s ∧ C Assign if x ∈ FV(s) S {E σ ∧ x s | E σ ∈ Σ} E rep(x s, C) S Σ E x f (ū n ) ∧ C Uvar if x ∈ FV(f (ū n )) S Σ E [t]∈E cc , f ( tn)∈[t] (x t ∧ u 1 t 1 ∧ • • • ∧ u n t n ∧ C) S Σ E f (ū n ) f (s n ) ∧ C Ucomp S Σ E (u 1 s 1 ∧ • • • ∧ u n s n ∧ C) ∨ [t]∈E cc , f ( tn)∈[t], f ( t n )∈[t] u 1 t 1 ∧ • • • ∧ u n t n ∧ s 1 t 1 ∧ • • • ∧ s n t n ∧ C S Σ E f (ū n ) g(s m ) ∧ C Ugen S Σ E [t]∈E cc , f ( tn)∈[t], g( t m )∈[t] u 1 t 1 ∧ • • • ∧ u n t n ∧ s 1 t 1 ∧ • • • ∧ s m t m ∧ C if f = g S Σ E x y ∧ C Dvar S Σ E [t], [t ]∈E cc , E|=t t (x t ∧ y t ∧ C) S Σ E x f (s n ) ∧ C Dfapp S Σ E [t], [t ]∈E cc , E|=t t , f ( t n )∈[t ] (x t ∧ s 1 t 1 ∧ • • • ∧ s n t n ∧ C) S Σ E f (ū n ) g(s m ) ∧ C Dgen S Σ E [t], [t ]∈E cc , E|=t t , f ( tn)∈[t], g( t m )∈[t ] u 1 t 1 ∧ • • • ∧ u n t n ∧ s 1 t 1 ∧ • • • ∧ s m t m ∧ C S Σ E C 1 ∧ C 2 Split ∧ S (Σ E C 1 ) (Σ E C 2 ) S Σ E C 1 ∨ C 2 Split ∨ S (Σ E C 1 ) (Σ E C 2 ) S (Σ E C Σ E C ) Meet S Eσ∈Σ, E σ ∈Σ {E σ } E C ∧ rep(E σ , E σ ) ∧ rep(E σ , C ) S (Σ E c 1 Σ E c 2 ) Join with c 1 , c 2 ∈ {⊥, } S Σ ∪ Σ E c 1 ∨ c 2 S Σ E ∧ C Fail ∧ if is ground and E |= S ∅ E ⊥ S Σ E ∧ C Yield ∧ if E |= S Σ E C S Σ E ∨ C Fail ∨ if is ground and E |= S Σ E C S Σ E ∨ C Yield ∨ if E |= S Σ E
E = {f (a) f (b), h(a) h(c), g(b) h(c)} L = {h(x 1 ) h(c), h(x 2 ) g(x 3 ), f (x 1 ) f (x 3 ), x 4 g(x 5 )} E cc = {{a}, {b}, {c}, {f (a), f (b)}, {h(a), h(c)}, {g(b)}}
The derivation on the respective E-ground (dis)unification problem, with the above strategy, is shown below. As before, the solving of x 4 g(x 5 ) is kept implicit to simplify the presentation.

Steps with double lines represent numerous applications of the indicated rules, e.g.:

{ } E f (x 1 ) f (x 3 ) ∧ h(x 2 ) g(x 3 ) ∧ h(x 1 ) h(c) Split * ∧ { } E f (x 1 ) f (x 3 ) { } E h(x 2 ) g(x 3 ) { } E h(x 1 ) h(c)
We present the derivation on each solving statement independently. The statement for the first constraint, { } E f (x 1 ) f (x 3 ), is reduced in the following manner:

{ } E f (x 1 ) f (x 3 ) Ucomp { } E x 1 x 3 ∨ (x 1 a ∧ x 3 b) ∨ (x 1 b ∧ x 3 a) Split * ∨ { } E x 1 x 3 { } E x 1 a ∧ x 3 b { } E x 1 b ∧ x 3 a Assign * {{x 1 x 3 }} E {{x 1 a, x 3 b}} E {{x 1 b, x 3 a}} E Join * , Yield ∨ {{x 1 x 3 }, {x 1 a, x 3 b}, {x 1 b, x 3 a}} E while { } E h(x 2 ) g(x 3
) is reduced as

{ } E h(x 2 ) g(x 3 ) Dgen { } E (x 2 c ∧ x 3 b) ∨ (x 2 a ∧ x 3 b) Split ∨ { } E x 2 c ∧ x 3 b { } E x 2 a ∧ x 3 b Assign * {{x 2 c, x 3 b}} E {{x 2 a, x 3 b}} E Join * {{x 2 c, x 3 b}, {x 2 a, x 3 b}} E and { } E h(x 1 ) h(c) as { } E h(x 1 ) h(c) Ucomp { } E x 1 c ∨ x 1 a Split ∨ { } E x 1 c { } E x 1 a Assign * {{x 1 c}} E {x 1 a} E Join {{x 1 c}, {x 1 a}} E
The global derivation is resumed below with the results from the above ones. The remaining steps to perform in the strategy are to combine the interdependent solutions and simplify the resulting constraints. To improve the presentation, let

Σ 1 = {{x 1 x 3 }, {x 1 a, x 3 b}, {x 1 b, x 3 a}} Σ 2 = {{x 2 c, x 3 b}, {x 2 a, x 3 b}} Σ 3 = {{x 1 c}, {x 1 a}}
Moreover, the presentations of the combinations are collapsed. The results from Meet lead to several solving statements to be combined with Join, besides the built constraints being amenable to assignments and conjunctive and disjunctive simplifications. Thus only the final results are depicted for the combinations of Σ 2 with Σ 3 and then of its result with Σ 1 .

{ } E f (x 1 ) f (x 3 ) ∧ h(x 2 ) g(x 3 ) ∧ h(x 1 ) h(c) . . . This strategy can be optimised in numerous ways, such as applying Fail ∧ as soon as possible and then "propagating" the failure through other statements with Meet. Similarly, applying

Σ 1 E Σ 2 E Σ 3 E Σ 1 E            {x 1 c, x 2 c, x 3 b}, {x 1 c, x 2 a, x 3 b}, {x 1 a, x 2 c, x 3 b}, {x 1 a, x 2 a, x 3 b}            E {x 1 a, x 2 c, x 3 b},
Meet as soon as a small set of solutions is obtained, which would then limit the number of possibilities to search in the interdependent statements, is another point of improvement. The main advantages of this calculus are in providing more flexibility for applying different search strategies while solving E-ground (dis)unification. Indeed it can emulate the previous calculus with a strategy that never applies the rule Split ∧ , and therefore also not Meet. This ensures that each branch is solved independently and has at most one solution. The last steps in the solving would be to apply a series of Join to gather all found solutions and close the derivation with series of Yield ∨ or Fail ∨ applications.

Chapter 5

Implementation

CCFV has been implemented in the veriT [START_REF] Bouton | veriT: An Open, Trustable and Efficient SMT-Solver[END_REF] and CVC4 [START_REF] Barrett | CVC4[END_REF] SMT solvers. We here describe the specifics of the implementation in veriT. As is common in CDCL(T ) based solvers, an E -graph data structure is kept internally to represent the set of signature classes E cc and efficiently check ground entailment modulo the theory of equality. This data structure is generated by the congruence closure decision procedure for ground equational first-order logic.

The E -graph is the basis for the indexing techniques described below. They are paramount for a practical procedure, allowing fast retrieval of candidates when searching for solutions for a given Dgen. However, as our experiments show, they are still effective in practice. Another limitation, but less relevant, is that the E -graph allows checking in constant time for equality only for terms known by the data structure. These are generally the ground terms appearing in the original formula. Checking whether e.g. two ground function applications f (t 1 , . . . , t n ), f (t 1 , . . . , t n ), that do not occur in the E-graph but may appear when analyzing L, are congruent requires checking whether all arguments, position by position, are congruent. Therefore the operation is worst-case linear in the size of the terms. As before, this does impact significantly the performance of the implementation.

Indexing

Indexing

Performing E-ground (dis)unification requires dealing with many terms, which makes the use of efficient indexing techniques for fast retrieval of candidates paramount for efficiency. Besides the indexing, we also discuss how the ground model E is minimised to reduce the number of terms that need to be considered. All operations below rely on terms being represented internally as directed acyclic graphs (DAGs) with maximal sharing, also known as "hash-consing", of common expressions. Therefore terms can be traversed as DAGs and syntactic equality between terms can be checked in constant time. reps(f ): yields all representatives whose respective signature class in E cc contains fapplications. The representatives are collected from the entries in the index for f . This operation is linear on the size of the index result for f .

apps(f, s): yields all f -applications in class(s). They are retrieved by traversing the set of terms in class(s) and collecting those whose top symbol is f . This operation is linear on the size of class(s).

apps(f ): yields all f -applications occurring in E cc , which amounts to collecting all terms indexed for f . This operation is constant time, since f is mapped in the index to what corresponds to apps(f ).

diseqs(s): yields all representatives of terms in E cc disequal to s, according to E. This operation is implemented in constant time by associating, to each signature class, a previously computed ordered list of the representatives of classes containing terms disequal to it.

This way it is possible to check if two ground terms t 1 and t 2 are disequal by assessing whether find(t 1 ) occurs in diseqs(t 2 ), or vice-versa, depending on which one is smaller. By keeping an ordered list, the occurrence check can be done on the logarithm of the list's size.

To enumerate all terms in E cc disequal to s it suffices to collect

t ∈ diseqs(s) class(t)
which can be done in linear time on the size of diseqs(s).

To optimise these operations we use approximated sets, as in the Simplify [START_REF] Detlefs | Simplify: A Theorem Prover for Program Checking[END_REF] and Z3 [START_REF] De | Efficient E-Matching for SMT Solvers[END_REF] systems. They behave much in the same way as sets, except that membership and overlap tests may return false positives. Each signature class is associated with an approximated set containing the functions symbols which have applications in that class. This technique allows checking if a symbol has applications in a signature class in constant time for a subset of the total set of symbols. If e.g. one is querying with apps(f, s) for all f -applications in [s], this result cannot be empty if f is in the approximated set of [s]. These approximated sets are implemented with bit masks: each symbol is assigned an arbitrary bit, and the mask for the class is a vector of bits. The set positions are those for which the respective symbol has applications in the class.

Model Minimisation For efficiency reasons, the E-graph in veriT, as in other CDCL(T ) solvers, contains not only the terms occurring in the current E but all ground terms from the original input formula. This means that a top symbol index built directly from the E-graph will generally contain more terms than actually appear in E. When using operations such as apps(f ) more terms will be considered, and therefore generally more instances generated, than it would be the case if one were to consider only the terms in E. This has the side effect of potentially worsening the already explosive nature of trigger based instantiation.

To tackle this issue we have two alternative ways of building the top symbol indexing in veriT. The first way considers the E-graph, as explained above. The second one collects terms directly from E by traversing the currently asserted literals. As with the E-graph, only a single term is kept per signature. Dealing directly with the ground model also has the advantage of allowing its minimisation. Since the SAT solver generally asserts more literals than necessary, the propositional abstraction of E ∪Q generally can be pruned while still propositionally entailing the original formula. This minimisation is done by computing a prime implicant, a minimal partial assignment. Its computation can be performed in linear time (see e.g. Déharbe et al. [START_REF] Déharbe | Computing Prime Implicants[END_REF]).

By having a smaller E one reduces the search space to consider when solving an E-ground (dis)unification problem. Another possibility is to minimise E cc , i.e. complementing E with equalities between its terms until the number of signature classes is as small as possible. This minimisation problem, however, is NP-complete [START_REF] Reynolds | Finite Model Finding in SMT[END_REF], so we do not attempt it. Moreover, it is not necessary for the effectiveness of the instantiation techniques we implement.

We also clean the CNF overhead: we remove part of the propositional variables introduced by the non-equivalency preserving CNF transformation the formula undergoes. They have the side effect that the prime implicant for the CNF is not necessarily prime for the original formula.

We apply the same process as de Moura and Bjørner [START_REF] De | Efficient E-Matching for SMT Solvers[END_REF] for Relevancy.

Example 5.1 ([dMB07]). To illustrate the issue, consider a clause 1 ∨( 2 ∧ 3 ). Its clausification using a Tseitin [START_REF] Tseitin | On the Complexity of Derivation in Propositional Calculus[END_REF] style algorithm yields the set of clauses

{ 1 , aux }, { aux , ¬ 2 , ¬ 3 }, { 2 , ¬ aux }, { 3 , ¬ aux }
Now, suppose that 1 is assigned true. In this case, 2 and 3 are clearly irrelevant and truth assignments to 2 and 3 need not be used, but this fact is occulted by the Tseitin encoding, which creates a set of clauses.

To determine which literals are relevant one can traverse the original formula using the Boolean valuations derived from the prime implicant. Then only the literals which are required to make the formula true are marked as relevant and kept in the propositional assignment from which E ∪ Q is derived.

Finding solutions

We present in Figure 5.1 an abstract algorithm to solve E-ground (dis)unification. It implements the backtracking CCFV calculus described in Section 4.2 with the strategy from Section 4.2.1.

The same notation conventions for ground and non-ground terms from Section 4 are used. The algorithm takes as input a partial solution and a conjunctive set of constraints to be entailed.

It produces the set of all complete solutions for the input constraints which extend the input solution. Of course, this set may be empty if there is no such extension. Thus, an initial call CCFV( , L) yields the set of solutions {E 1 σ , . . . , E n σ }, from which all ground solutions σ * , such that σ is acyclic and ran(σ * ) ⊆ T(E ∪ L), are derivable. From now on we ambiguously refer to the algorithm as CCFV, clarifying when necessary whether we mean the algorithm or the calculus.

The set of constraints on which CCFV operates are kept as a stack of pairs of terms to be entailed equal of disequal. The most simple implementation of sel is to merely pop the a field for the respective variable; a flag to whether that variable is the representative of its congruence class; a field for, if the variable is a representative, the ground term or non-ground function application it is equal to; otherwise a pointer to the variable it is equal to, the default being itself.

else if t 1 = f (s n ) and t 2 = f (r n ) then return CCFV(E σ , C ∪ {s 1 r 1 , . . . , s n r n }) return ∅ x s : if x ∈ FV(s) then // Assignment E σ ← E σ ∪ {x s}; C ← rep(C) return CCFV(E σ , C) else // s is a non-ground function application let s = f (ū n ) in for t ∈ reps(f ) do // Uvar Sols ← Sols ∪ CCFV(E σ , C ∪ {f (ū n ) t, x t}) return Sols f (ū n ) t : // E -matching for f ( tn ) ∈ apps(f, t) do Sols ← Sols ∪ CCFV(E σ , C ∪ {u 1 t 1 , . . . , u n t n }) return Sols f (ū n ) g(ū n ) : if f = g then // E -
These solutions are manipulated with a UNION-FIND algorithm with path-compression. The union operation is made modulo the congruence closure on the ground terms and the current assignments to the variables in that solution. The operation keeps the invariant that the solution is a consistent set of equalities. CCFV keeps a single global candidate solution that is updated by adding or removing assignments, according to how the search proceeds. An specialised E-graph is used for the terms in L, such that constraints are considered modulo the current solution. The E-graph is updated as the current solution changes, merging classes or backtracking these merges as assignments are added or removed from the solution. When an actual solution is found, i.e. when all constraints have been solved for a given candidate solution, a copy of the found solution is stored in a global accumulator of solutions.

CCFV performs a depth-first search for solutions. Given a partial solution and a conjunctive set of constraints, it selects a given constraint; determines how to handle it according to its structure; augments the current solution, and thus also the remaining constraints, if necessary, or try all possibilities for entailing the respective constraint according to the indexing of E cc ; and then proceeds to solve the remaining constraints. Each loop through different unification possibilities effectively introduces "break-points" in the search. The remaining constraints are augmented and the search proceeds, but after that possibility is explored the executing will return to the break-point. All assignments that may have been added to the current solution will have been removed, all modifications to the E-graph backtracked, and the remaining constraints to consider will be as they were before the new ones had been added. This can be seen as a "branch" in the search being closed and a new one being picked to be explored. The solutions obtained from closed branches are stored in the solution accumulator. When all branches have been explored, i.e. all cases in the loop have been considered, the execution returns to the previous break-point, backtracking the solution and the E-graph accordingly, and then proceeds, until they have all been exhausted and the execution halts.

To optimise the search, the algorithm applies more case distinctions than the rules in Table 4.1, such as differentiating between E -matching and E -unification. It also makes use of the operations on the top symbol index and E-graph to reduce the number of terms that need to be considered in the search for solutions. assume that Assign is applied. Then the term f (g(x), y) becomes f (g(t), y) in the branch.

A necessary condition for the literal f (g(t), y) h(z) to be entailed is that there exists some

f (t 1 , t 2 ) ∈ T(E) such that E |= g(t) t 1 .
To efficiently implement this technique it is necessary to query with a function symbol and pairs of ground terms and positions whether there is any term in E cc with the same top symbol and whose arguments are congruent with the given ground terms in the respective positions.

The index operation would have the form apps(f, w 1 , .

Breadth-first CCFV

The above algorithm implements a depth-first search for solutions, following the backtracking CCFV calculus. Here we present an abstract algorithm in Figure 5.2. that implements the non-backtracking CCFV calculus described in Section 4.3 with the strategy from Section 4.3.1.

The algorithm, henceforth CCFV-breadth, takes as input a conjunctive set of constraints to be entailed. It produces the set of all solutions for the input constraints. Of course, as before, this set may be empty if there are no solutions. CCFV-breadth uses the same data structures as its depth-first counterpart. However, it explicitly manipulates the different partial solutions produced during the solving. Moreover, since in this strategy the variable assignments only occur when the remaining constraints are ground, there is no need to have an E-graph for the terms in L to be updated according to assignments.

The algorithm also has break-points with recursive calls from within loops of independent possibilities. However, the recursive call contains only "local constraints", generated from the analysis of the currently selected constraint. After the call is finished, the results are combined with those from previously selected constraints. This way, constraints are solved independently and the found solutions are combined according to how these constraints have been generated.

The crucial operations in CCFV-breadth are the combination operations, i.e. the implementations of Join and Meet. They are represented in the algorithm by the symbols and , respectively, and are performed directly on sets of solutions. For now we have naïve implementations of these combinations. The data structure we use for representing solutions is not optimised h(c) be the first constraint considered in the outer while loop. The possibilities to solve h(x 1 ) h(c) are enumerated in the E -matching case. This constraint is solved independently and the obtained orthogonal solutions are c-sols = {{x 1 a}, {x 1 c}} Let the selection function next consider the constraint h(x 2 ) g(x 3 ). Independently solving this constraint yields c-sols = {{x 2 c, x 3 b}, {x 2 a, x 3 b}} These solutions are then merged with the solutions from the previous constraint, forming the global set of solution

function CCFV(C) is Sols ← { } while C = ∅ and Sols = ∅ do // Select constraint c ← sel(C); C ← C \ {c}; c-sols ← { } match c with t 1 t 2 : // Ground disequality if t 1 ∈ diseqs(t 2 ) then c-sols ← ∅ t 1 t 2 : // Ground equality if t 1 , t 2 ∈ T(E) then if find(t 1 ) = find(t 2 ) then c-sols ← ∅ else if t 1 = f (s n ) and t 2 = f (r n ) then c-sols ← CCFV({s 1 r 1 , . . . , s n r n }) else c-sols ← ∅ x s : if x ∈ FV(s) then // Assignment c-sols ← {x s} else // s is a non-ground function application let s = f (ū n ) in for t ∈ reps(f ) do // Uvar c-sols ← c-sols CCFV({f (ū n ) t, x t}) f (ū n ) t : // E -matching for f ( tn ) ∈ apps(f, t) do c-sols ← c-sols CCFV({u 1 t 1 , . . . , u n t n }) f (ū n ) g(ū n ) : if f = g then // E -unify arguments c-sols ← c-sols CCFV({u 1 u 1 , . . . , u n u n }) for t ∈ reps(f ) do // E -matching into same class c-sols ← c-sols CCFV({f (ū n ) t, g(ū n ) t}) x t : for t ∈ diseqs(t) do // Assignment into a disequal term c-sols ← c-sols CCFV({x t }) f (ū n ) t : // E -matching into a disequal term for t ∈ diseqs(t) do c-sols ← c-sols CCFV({f (ū n ) t }) x f (ū n ) : // Dfapp for t ∈ reps(f ) do c-sols ← c-sols CCFV({f (ū n ) t, x t}) f (ū n ) g(ū n ) : // E -matching into disequal terms for t ∈ reps(f ) do c-sols ← c-sols CCFV({f (ū n ) t, g(ū n ) t}) x y : //
Sols = {{x 1 a}, {x 1 c}} {{x 2 c, x 3 b}, {x 2 a, x 3 b}} =            {x 1 c, x 2 c, x 3 b}, {x 1 c, x 2 a, x 3 b}, {x 1 a, x 2 c, x 3 b}, {x 1 a, x 2 a, x 3 b}           
By proceeding analogously the CCFV-breadth algorithm will find the same solutions as in Example 4.11 pretty much in the same way.

Memoization Quite often CCFV-breadth needs to look for solutions for the same E-ground (dis)unification problem. To avoid duplication of work, we store the result of solving constraints.

Thus whenever that constraint is met again the respective solutions may be directly retrieved from the memory instead of recomputed. For now we have only a coarse index for constraints, but the technique is nevertheless effective in making CCFV-breadth faster.

A more ambitious application of memoization is to keep the results of solving constraints across different calls to the instantiation module. This would allow updating the stored results according to how the candidate assignment E ∪ Q changed, as the theory solvers do in the CDCL(T ) framework. This is a possibility for having an incremental CCFV algorithm, however its viability has not been tested in a practical implementation.

Applying instantiation techniques

We here describe how to implement trigger and conflict based instantiation on top of CCFV.

We leave the implementation of model based instantiation, whose theoretical suitability we have outlined in the previous chapter, for future work. In veriT we have also not yet implemented the functionality to discard instances generated from triggers that are already entailed nor the eventual propagation of equalities as a byproduct of failed search for conflicting instances.

Trigger based instantiation We follow the guidelines from Leino and Pit-Claudel [START_REF] K. Rustan | Trigger Selection Strategies to Stabilize Program Verifiers[END_REF] outlined in Section 3.2.1 for selecting triggers. For a given quantified formula with a trigger T = {u 1 , . . . , u n }, solving the E-ground (dis)unification

E |= (u 1 y 1 ∧ • • • ∧ u n y n ) σ
with the restriction that all y i must be grounded, provides all the desired trigger instantiations.

Instead of changing the CCFV algorithm to perform the restricted search, we use an outer loop that directly builds the E-ground (dis)unification problems in which ȳn have been grounded.

The terms enumerated for grounding ȳn are retrieved from apps(f ). CCFV can then be applied straightforwardly to collect the solutions. All found solutions are used for building instantiation lemmas.

b : implements the breadth-first version of CCFV rather than the depth-first one (see Section 5.2.1); e : optimization for eagerly discarding branches with unmatchable applications (see "Discarding unsuitable branches" in Section 5.2); d : discards already entailed trigger based instances (see "Discarding entailed instances" in Section 4.2.3)

The configuration verit refers to the previous version of veriT, which only offered support for quantified formulas through naïve trigger instantiation, without further optimizations. The configuration cvc refers to version 1.5 of CVC4, which applies t and c by default, as well as propagation of equalities. Both veriT and CVC4 implement efficient term indexing and apply a simple selection heuristic, checking ground and reflexive literals first but otherwise considering the conjunction of constraints as a queue. The breadth-first variation of CCFV is implemented only in veriT, using the simple strategy described in Sections 5.4 and 4.3.1.

The evaluation was made on the UF, UFLIA, UFLRA and UFIDL categories of SMT-LIB [START_REF] Barrett | The SMT-LIB Standard: Version 2.5[END_REF], with 10 495 benchmarks annotated as unsatisfiable5 , mostly stemming for verification and ITP platforms. The categories with bit vectors and non-linear arithmetic are currently not supported by veriT and in those in which uninterpreted functions are not predominant the techniques shown here are not as effective. Since veriT cannot produce models for formulas with quantifiers and the finite-model finding techniques in CVC4 are not affected by CCFV, only unsatisfiable problems were considered. Our experiments were conducted using machines with 2 CPUs Intel Xeon E5-2630 v3, 8 cores/CPU, 126GB RAM, 2x558GB HDD. The timeout was set for 30 seconds, since our goal is evaluating SMT solvers as back-ends of verification and ITP platforms, which require fast answers.

Figure 5.3 exhibits an important impact of CCFV and the techniques and optimizations built on top of it. verit+t performs much better than verit, solely due to CCFV. Moreover, verit+tc presents a significant improvement in terms of problems solved (474 more against 36 less) by the use of the conflict based instantiation, but it also shows a less clear gain of time. Besides the difficulty to predict how combining any given technique with trigger based instantiation will affect performance, we believe that this less clear gain in time is due to the more expensive search performed: trying to falsify quantified formulas and handling full E-ground (dis)unification, which, in the context of SMT, has a much bigger search space than simply performing E -matching for pattern-matching instantiation. Not always the "better quality" of the conflicting instances offsets the time it took to compute them, which indicates the necessity to identify beforehand such cases and avoid the more expensive search when counter-productive. A comparison of both flavours of CCFV is shown in Figure 5.4. Both variations perform well, with the depth-first CCFV outperforming its breadth-first counterpart by a small margin. This shows that both approaches are viable. cvc+d and cvc+e improve significantly over cvc, exhibiting The comparison between the different configurations of veriT and CVC4 with the SMT solver Z3 (version 4.4.2) is summarised in Table 5.1, excluding categories (such as UFLRA) whose problems are trivially solved by all systems, which leaves 8 701 problems for consideration. The table exhibits the total number of problems solved by each configuration within the timeout. verit+tc solves approximately 800 more problems than verit, solving approximately the same total number of problems than Z3. Many of these new problems come from the sledgehammer benchmarks, which contain less theory symbols and whose solving relies more on equational first-order logic.

Moreover, verit+tc performs best in the grasshopper families, stemming from the heap verification tool GRASShopper [START_REF] Piskac | GRASShopper -Complete Heap Verification with Mixed Specifications[END_REF]. Considering the overall performance, both cvc+d and cvc+e solve significantly more problems than cvc, specially in benchmarks from verification platforms, approaching the performance of Z3 in these families. Both these techniques, as well as the propagation of equalities, are fairly important points in the performance of CVC4, so their implementation is a clear direction for improvements in veriT.

Part II

Proof Production

Chapter 6

Processing calculus

An increasing number of automatic theorem provers can generate certificates, or proofs, that justify the formulas they derive. These proofs can be checked by other programs and shared across reasoning systems. Some users will also want to inspect this output to understand why a formula holds. Proof production is generally well understood for the core proving methods and for many theories commonly used in satisfiability modulo theories (SMT). But most automatic provers also perform some formula processing or preprocessing-such as clausification and rewriting with theory-specific lemmas-and proof production for this aspect is less mature.

For most provers, the code for processing formulas is lengthy and deals with a multitude of cases, some of which are rarely executed. Although it is crucial for efficiency, this code tends to be given much less attention than other aspects of provers. Developers are reluctant to invest effort in producing detailed proofs for such processing, since this requires adapting a lot of code. As a result, the granularity of inferences for formula processing is often coarse. Sometimes, processing features are even disabled to avoid gaps in proofs, at a high cost in proof search performance.

Fine-grained proofs are important for a variety of applications. We propose a framework to generate such proofs without slowing down proof search. This chapter describes a proof calculus in which to generate fine-grained proofs for processing formulas. The next chapter introduces an scalable framework for generating such proofs. The work described in both chapters led to a joint publication with Jasmin Blanchette and Pascal Fontaine [START_REF] Barbosa | Scalable Fine-Grained Proofs for Formula Processing[END_REF].

Conventions For the following chapters, we assume that our language for many-sorted firstorder logic with equality contains two more binders besides the quantifiers: Hilbert's choice operator εx. ϕ and a 'let' construct, let xn sn in t, which simultaneously assigns n variables that can be used in the body t.

As before, we use the symbol = for syntactic equality on terms. The symbol = α stands for syntactic equality up to renaming of bound variables. We reserve the names a, c, f, g, p, q for function symbols; x, y, z for variables; r, s, t, u for terms (which may be formulas); ϕ, ψ for formulas; and Q for quantifiers (∀ and ∃).

|= ∃x. ϕ[x] -→ ϕ[εx. ϕ] (ε 1 ) |= (∀x. ϕ ψ) -→ (εx. ϕ) (εx. ψ) (ε 2 ) |= (let xn sn in t[x n ]) t[s n ] (let)
The property (ε 2 ) may seem unnecessary, but it provides determinism for the choice operator.

In particular, it ensures that reflexivity holds for terms involving ε, such that the substitution of equals for equals is correct for such terms.

Inference system

The inference rules used by our framework depend on a notion of context defined by the grammar

Γ ::= ∅ | Γ, x | Γ, xn → sn
The empty context ∅ is also denoted by a blank. Each context entry either fixes a variable x or defines a substitution {x n → sn }. Any variables arising in the terms sn will normally have been introduced in the context Γ on the left. If a context introduces the same variable several times, the rightmost entry shadows the others.

Abstractly, a context Γ fixes a set of variables and specifies a substitution subst(Γ). The substitution is the identity for ∅ and is defined as follows in the other cases:

subst(Γ, x) = subst(Γ)[x → x] subst(Γ, xn → tn ) = subst(Γ) • {x n → tn }
In the first equation, the [x → x] update shadows any replacement of x induced by Γ. The examples below illustrate this subtlety:

subst(x → 7, x → g(x)) = {x → g(7)} subst(x → 7, x, x → g(x)) = {x → g(x)}
We write Γ(t) to abbreviate the capture-avoiding substitution subst(Γ)(t).

Transformations of terms (and formulas) are justified by judgments of the form Γ t u,

where Γ is a context, t is an unprocessed term, and u is the corresponding processed term. The free variables in t and u must appear in the context Γ. Semantically, the judgment expresses the equality of the terms Γ(t) and u for all variables fixed by Γ. Crucially, the substitution applies only on the left-hand side of the equality.

The inference rules for the transformations covered in this thesis are presented below, followed by explanations.

Taut T if |= T Γ(t) u Γ t u Γ s t Γ t u Trans if Γ(t) = t Γ s u Γ t i u i n i=1 Cong Γ f( tn ) f(ū n ) Γ, y, x → y ϕ ψ Bind if y / ∈ FV(Qx. ϕ) Γ (Qx. ϕ) (Qy. ψ) Γ, x → (εx. ϕ) ϕ ψ Sko ∃ Γ (∃x. ϕ) ψ Γ, x → (εx. ¬ ϕ) ϕ ψ Sko ∀ Γ (∀x. ϕ) ψ Γ r i s i n i=1 Γ, xn → sn t u
Let if Γ(s i ) = s i for all i ∈ [n] Γ (let xn rn in t) u -Taut T relies on an oracle |= T to derive arbitrary lemmas in a theory T. In practice, the oracle will produce some kind of certificate to justify the inference. An important special case, for which we use the name Refl, is syntactic equality (up to renaming of bound variables); the side condition is then Γ(t) = α u. (We use = α instead of = because applying a substitution can rename bound variables.) -Trans needs the side condition because the term t appears both on the left-hand side of (where it is subject to Γ's substitution) and on the right-hand side (where it is not).

Without the side condition, the two occurrences of t in the antecedent could denote different terms.

-Cong can be used for any function symbol f, including the logical connectives.

-Bind is a congruence rule for quantifiers. The rule also justifies the renaming of the bound variable(from x to y). The side condition prevents an unwarranted variable capture. In the antecedent, the renaming is expressed by a substitution in the context. If x = y, the context is Γ, x, x → x, which has the same meaning as Γ, x.

-Sko ∃ and Sko ∀ exploit (ε 1 ) to replace a quantified variable with a suitable witness, simulating skolemization. We can think of the ε expression in each rule abstractly as a fresh function symbol that takes any fixed variables it depends on as arguments. In the antecedents, the replacement is performed by the context.

-Let exploits (let) to expand a 'let' expression. Again, a substitution is used. The terms rn assigned to the variables xn can be transformed into terms sn .

The antecedents of all the rules inspect subterms structurally, without modifying them. Modifications to the term on the left-hand side are delayed; the substitution is applied only in Taut. This is crucial to obtain compact proofs that can be checked efficiently. Some of the side conditions may look computationally expensive, but there are ways to compute them fairly efficiently. Furthermore, by systematically renaming variables in Bind, we can satisfy most side conditions trivially, as we will prove in Sect. 6.2.

The set of rules can be extended to cater for arbitrary transformations that can be expressed as equalities, using Hilbert choice to represent fresh symbols if necessary. The usefulness of Hilbert choice for proof reconstruction is well known [dNiv05, PS07, BW10], but we push the idea further and use it to simplify and uniformize the inference system.

Example 6.1. The following derivation tree justifies the expansion of a 'let' expression: The Cong inference above Sko ∀ is optional; we could have directly closed the derivation with Refl. In a prover, the term ε x would be represented by a fresh Skolem constant c, and we would ignore c's connection to ε x during proof search.

Skolemization can be applied regardless of polarity. Normally, we skolemize only positive existential quantifiers and negative universal quantifiers. However, skolemizing other quantifiers is sound in the context of proving. The trouble is that it is generally incomplete, if we introduce Skolem symbols and forget their definitions in terms of Hilbert choice. To paraphrase Orwell, all quantifiers are skolemizable, but some quantifiers are more skolemizable than others. In the above, Γ 1 = x, x → x; Γ 2 = Γ 1 , x → f(x); and Γ 3 = Γ 2 , y → f(x). The inference marked with an asterisk (*) is illegal, because Γ 2 (f(x)) = f(f(x)) = f(x). We exploit this to derive an invalid judgment, with a spurious application of f on the right-hand side. To apply Let legally, we must first rename the universally quantified variable x to a fresh variable z using the Bind rule: This time, we have Γ 1 = z, x → z; Γ 2 = Γ 1 , x → f(z); and Γ 3 = Γ 2 , y → f(z). Let's side condition is satisfied: Γ 2 (f(z)) = f(z).

Example 6.5. The dangers of capture are illustrated by the following tree, where ε y stands for εy. p(x) ∧ ∀x. q(x, y):

Refl*

x, y → ε y (p(x) ∧ ∀x. q(x, y)) (p(x) ∧ ∀x. q(x, ε y ))

Sko ∃
x (∃y. p(x) ∧ ∀x. q(x, y)) (p(x) ∧ ∀x. q(x, ε y )) Bind (∀x. ∃y. p(x) ∧ ∀x. q(x, y)) (∀x. p(x) ∧ ∀x. q(x, ε y ))

The inference marked with an asterisk would be legal if Refl's side condition were stated using a capturing substitution. The final judgment is unwarranted, because the free variable x in the first conjunct of ε y is captured by the inner universal quantifier on the right-hand side.

To avoid the capture, we rename the inner bound variable x to z. Then it does not matter if we use a capture-avoiding or a capturing substitution:

Refl

x, y → ε y p(x) p(x)

Refl

x, y → ε y , x → z q(x, y) q(z, ε y ) Bind x, y → ε y (∀x. q(x, y)) (∀z. q(z, ε y ))

Cong

x, y → ε y (p(x) ∧ ∀x. q(x, y)) (p(x) ∧ ∀z. q(z, ε y ))

Sko ∃
x (∃y. p(x) ∧ ∀x. q(x, y)) (p(x) ∧ ∀z. q(z, ε y )) Bind (∀x. ∃y. p(x) ∧ ∀x. q(x, y)) (∀x. p(x) ∧ ∀z. q(z, ε y ))

Soundness

To prove the soundness of the processing calculus we start by encoding the judgments in a wellunderstood theory of binders: the simply typed λ-calculus. A context and a term will be encoded together as a single λ-term. We call these somewhat nonstandard λ-terms metaterms. They are defined by the grammar M ::= t | λx. M | (λx n . M ) tn where x i and t i are of the same sort for each i ∈ [n]. A metaterm is either a term t decorated with a box , a λ-abstraction, or the application of an n-tuple of terms to an uncurried λabstraction that simultaneously binds n distinct variables. We let = αβ denote syntactic equality modulo α-and β-equivalence (i.e., up to renaming of bound variables and reduction of applied λ-abstractions). We use the letters M, N, P to refer to metaterms. The notion of type is as expected for simply typed λ-terms: The type of t is the sort of t; the type of λx. M is σ → τ , where σ is the sort of x and τ the type of M ; and the type of (λx n . M ) tn is the type of M . It is easy to see that all metaterms contain exactly one boxed term. M [t] denotes a metaterm whose box contains t, and M [N ] denotes the same metaterm after its box has been replaced with the metaterm N.

Encoded judgments will have the form M N. The λ-abstractions and applications represent the context, whereas the box stores the term. To invoke the theory oracle |= T , we will need to reify equalities on metaterms-i.e., map them to equalities on terms. Let M, N be metaterms of type σ 1 → • • • → σ n → σ. We define reify(M N ) as ∀x n . t u, where M = αβ λx 1 . . . . λx n . t and N = αβ λx 1 . . . . λx n . u . Thanks to basic properties of the λ-calculus, t and u are always defined uniquely up to the names of the bound variables. For example, if M = λu. (λv. p(v) ) u and N = λw. q(w) , we have M = αβ λx. p(x) and N = αβ λx. q(x) , and the reification of M N is ∀x. p(x) q(x).

The inference rules presented in Sect. 6.1 can now be encoded as follows. We refer to these new rules collectively as the encoded inference system: call is bounded by a constant (3, in build-app for simplification).

Notice that all arguments to apply must be computed regardless of the apply calls. If an apply call takes constant time, the proof generation overhead is linear in the size of the input.

To achieve this performance, it is necessary to use sharing to represent contexts and terms in the output; otherwise, each call to apply might itself be linear in the size of its arguments, resulting in a nonlinear overhead on the generation of the entire proof.

Observation 7.5 (Cost of Proof Checking). Checking an inference step can be performed in constant time if checking the side condition takes constant time.

Justification. The inference rules involve only shallow conditions on contexts and terms, except in the side conditions. Using suitable data structures with maximal sharing, the contexts and terms can be checked in constant time.

The above statement may appear weak, since checking the side conditions might itself be linear, leading to a cost of proof checking that can be at least quadratic in the size of the proof (measured as the number of symbols that represent it). Fortunately, most of the side conditions can be checked efficiently. For example, for simplification (Sect. 7.1.3), the Bind rule is always applied with x = y, which implies the side condition y / ∈ FV(Qx. ϕ); and since no other rule contributes to the substitution, subst(Γ) is the identity. Thus, simplification proofs can be checked in linear time.

Moreover, certifying a proof by checking each step locally is not the only possibility. An alternative is to use an algorithm similar to the process function to check a proof in the same way as it has been produced. Such an algorithm can exploit sophisticated invariants on the contexts and terms.

Implementation

We implemented the contextual recursion algorithm and the transformations described in Sect. 7.1 in the SMT solver veriT [START_REF] Bouton | veriT: An Open, Trustable and Efficient SMT-Solver[END_REF], replacing large parts of the previous non-proof-producing, hard-to-maintain code. Even though it offers more functionality (proof generation), the preprocessing module is about 20% smaller than before and consists of about 3000 lines of code. There are now only two traversal functions instead of 10. This is, for us, a huge gain in maintainability. Besides, as our experimental data attests, we had no significant detrimental impact on the solving times or success rates, despite the production of detailed proofs.

Proofs

Previously, veriT provided detailed proofs for the resolution steps performed by the SAT solver and the lemmas added by the theory solvers and instantiation module. All transformations per-bit vectors and nonlinear arithmetic are not supported by veriT. Since veriT cannot produce models for formulas with quantifiers, only unsatisfiable problems were considered for this kind of benchmarks.

Our experiments were conducted on servers equipped with two Intel Xeon E5-2630 v3 processors, with eight cores per processor, and 126 GB of memory. Each run of the solver uses a single core. The time limit was set to 30 s, a reasonable value for interactive use within a proof assistant.

The These results indicate that the new generic contextual recursion algorithm and the production of detailed proofs do not impact performance negatively compared with the old code and coarse-grained proofs. Moreover, allowing Boolean and arithmetic simplifications leads to some improvements. We expect that generating proofs for the global transformations would lead to substantial improvements on quantifier-free problems. On benchmarks with quantifiers, as the experimental results indicate (e.g. the new code solves slightly more problems than the old one in the proof-producing configurations), it is very hard to predict the impact of novel techniques due to the nature of heuristic instantiation. This way, marginal changes such as these observed do not weaken our claim that there is no negative impact on performance by the production of detailed proofs.

Chapter 8

Conclusions

Our first contribution in this thesis has been the introduction of CCFV, a decision procedure for E-ground (dis)unification. We have shown how the main instantiation techniques of SMT solving may be based on it. We also discussed how to efficiently implement CCFV in a CDCL(T ) solver, a crucial aspect in our field of work. Our experimental evaluation shows that CCFV leads to significant improvements in the solvers CVC4 and veriT, making the former surpass the state-of-the-art in instantiation based SMT solving and the latter competitive in several benchmark libraries. The calculi presented are very general, allowing for different strategies and optimizations, as previously discussed.

There are three directions in which the work presented here can be improved: the CCFV solving, the reach of CCFV, and the instantiation techniques built on top of it. A direction for improving the solving is to use lemma learning in the depth-first CCFV, in a similar manner as SAT solvers do. When a branch fails to produce a solution and is discarded, analyzing the literals which led to the conflict can allow backjumping rather than simple backtracking, thus further reducing the solution search space. The Complementary Congruence Closure introduced by Backeman and Rümmer [START_REF] Backeman | Efficient Algorithms for Bounded Rigid Eunification[END_REF] could be extended to perform such an analysis. More generally, we believe that making CCFV incremental would allow significant performance gains, as it does for theory solvers. A starting point would be to build on techniques such as those described by de Moura and Bjørner [START_REF] De | Efficient E-Matching for SMT Solvers[END_REF] for performing incremental E -matching in Z3. The reach of CCFV can be extended by going beyond equational first-order logic. To support other theories the calculi have to be augmented with rules for the new interpreted symbols. To handle linear arithmetic, for instance, CCFV has to be able to perform AC1 unification (unification modulo associativity, commutativity and additive identity). Practical implementations will also require the ground solver to provide efficient entailment checks with relation to the new interpreted symbols, as it does for equality. Moreover, since decidability is easily lost when combining theories in quantified logic, a good balance must be achieved between decision procedures for specific fragments, such as the essentially uninterpreted fragment described by Ge and de Moura [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF], and effective heuristics for incomplete settings. Besides theory reasoning, higher-order unification could also be tackled by CCFV. The calculi would need to account for partial applications, functional Chapter 8. Conclusions variables, and lambda abstractions. This would allow SMT solvers to natively handle higherorder problems, thus avoiding completeness and performance issues with clumsy encodings into first-order logic. Yet another possible extension of CCFV is to handle rigid E -unification, so it could be integrated into tableaux and sequent calculi based techniques such as BREU [START_REF] Backeman | Theorem Proving with Bounded Rigid E-Unification[END_REF] or conflict resolution [START_REF] Slaney | Conflict Resolution: a First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning[END_REF]. This amounts to having non-ground equalities in E, which means significantly changing how CCFV works now. It would, however, allow integrating an efficient goal-oriented procedure into calculi that require solving E -unification problems.

CCFV can be seen as a first step towards a "theory solver" for quantified formulas to be integrated into a CDCL(T ) solver. Instantiation techniques built on top of CCFV would evaluate the candidate model with quantified formulas and: i) provide a finite-model when it exists, ii) derive instances refuting the candidate when they exist, iii) propagate relevant instantiations and iv) be incremental with relation to propositional assignments. Techniques from tableaux and superposition calculi, which natively consider quantified formulas simultaneously, could be combined with CCFV for solving the entailment above.

Our second contribution was to introduce a framework to represent and generate proofs of formula processing and its implementation in veriT and Isabelle/HOL. The framework centralises the subtle issue of manipulating bound variables and substitutions soundly and efficiently, and it is flexible enough to accommodate many interesting transformations. Although it was implemented in an SMT solver, there appears to be no intrinsic limitation that would prevent its use in other kinds of first-order, or even higher-order, automatic provers. The framework covers many preprocessing techniques and can be part of a larger toolbox. It allows veriT, whose detailed proofs have been one of its defining features, to produce more detailed justifications than ever.

However, there are still some global transformations for which the proofs are nonexistent or leave much to be desired. In particular, supporting rewriting based on global assumptions would be essential for proof-producing inprocessing, and symmetry breaking would be interesting in its own right. To support these transformations our notion of context would have to be extended, as well as the operations that are allowed to be performed on terms, in such a way that we can go beyond the replacement of equals by equals. The framework can also be extended to handle different language constructs, such as lambda abstractions. Given the generality of the processing calculus and the proof-producing algorithm, operations such as beta-reduction can be easily integrated. The latter, for instance, is merely a variation of 'let' expansion.

Our focus here has been in the production of detailed proofs, aiming to guarantee proof checking to have reasonable complexity and thus facilitate effective implementations of proof checkers. A promising direction is also to reconstruct the detailed proofs in proof assistants, which provide trustworthy, machine-checkable formal proofs of theorems. A general challenge is to perform within the proof assistants the necessary reasoning to check the proofs. For some theories, such as non-linear arithmetic, this can be quite challenging. Once possible, however, fully reconstructing proofs into proof assistants would greatly increase the overall confidence on the results of automatic solvers, thus avoiding the need to trust software that mostly rely on testing to perform sound logic reasoning.

In conclusion, we believe that our contributions are beneficial to the state-of-the-art of SMT solving (and consequentially also of first-order theorem proving). Moreover, given that both the frameworks presented are quite general and extensible, we expect them to serve as the starting point for several more techniques for instantiation and proof production in SMT solving, pushing solvers into tackling ever more expressive problems and producing more trustworthy results.

  Un problème central lors de l'application de techniques d'instanciation pour gérer des formules quantifiées en CDCL(T ) est comment déterminer les instances à dériver. Chacune des principales techniques, qu'il s'agisse des triggers, de conflits ou d'instanciation basée sur les modèles, contribuent grandement à l'efficacité des solveurs, mais chacune est généralement implémentée de manière indépendante, et avec ses propres structures de données. Dans le Chapitre 4, nous présentons un cadre uniforme pour le raisonnement avec des formules quantifiées dans la théorie de l'égalité et des fonctions non interprétées dans CDCL(T ). Nous présentons le problème d'E-ground (dis)unification comme algorithme central (Section 4.1), avec lequel les diverses techniques d'instanciation peuvent être implémentées. Ce problème concerne le problème classique de l'E -unification [DV98] rigide, un problème omniprésent dans le contexte des tableaux pour la logique équationnelle du premier ordre. En exploitant les similitudes entre CDCL(T ) et ces cadres, nous construisons sur des techniques classiques pour résoudre l'Eunification et présentons une procédure de décision pour l'E-ground (dis)unification: l'algorithme de Fermeture de congruence avec variables libres (congruence closure with free variables, CCFV) étend l'algorithme classique de fermeture de congruence [NO80, NO07], pour tenir compte des variables libres (Section 4.2). Nous montrons ensuite comment se baser sur CCFV pour implémenter une instanciation basée sur les triggers, sur les conflits ou sur les modèles (Chapitre 5).Ces chapitres décrivent le travail commun avec Pascal Fontaine et Andrew Reynolds[START_REF] Barbosa | Congruence Closure with Free Variables[END_REF].

  sur la pile. Les fonctions du plugin sont chargées d'invoquer apply selon le cas. L'algorithme effectue une récurrence contextuelle de post-profondeur en profondeur sur le terme à traiter. Les sous-termes sont traités en premier; Alors un terme intermédiaire est construit à partir des sous-termes résultants et est traité lui-même. Le contexte est mis à jour de manière spécifique à la transformation avec chaque appel récursif. Les fonctions du plugin sont divisées en deux groupes: celles qui mettent à jour le contexte lorsque l'algorithme entre dans le corps d'un quantificateur ou lorsqu'il passe d'un symbole de fonction à l'un de ses arguments; et celles qui renvoient le terme traité et produisent la preuve correspondante en effet de bord.ConclusionNotre première contribution dans cette thèse a été l'introduction de CCFV, une procédure de décision pour l'E-ground (dis)unification. Nous avons montré comment les principales techxx niques d'instanciation en SMT peuvent être basées sur elle. Nous avons également discuté de la manière d'implémenter efficacement CCFV dans un solver CDCL(T ), un aspect crucial dans notre domaine de travail. Notre évaluation expérimentale montre que CCFV conduit à des améliorations significatives dans les solveurs CVC4 et veriT, ce qui fait que l'ancien dépasse l'état de l'art en SMT avec instanciation. Les calculs présentés sont très généraux, permettant différentes stratégies et optimisations, comme nous l'avons déjà mentionné. Il existe trois directions dans lesquelles le travail présenté ici peut être amélioré: la résolution CCFV, la portée de CCFV et les techniques d'instanciation construites au delà de CCFV. Une direction pour améliorer la résolution est d'utiliser l'apprentissage de lemmas dans CCFV en profondeur d'abord, de la même manière que les solveurs SAT. Lorsqu'une branche ne parvient pas à produire une solution et qu'elle est rejetée, l'analyse des littéraux qui ont mené au conflit peut permettre le backjump plutôt qu'un simple backtracking, réduisant ainsi l'espace de recherche de la solution. L'algorithme Complementary Congruence Closure présenté par Backeman et Rümmer [BR15a] pourrait être étendu pour effectuer une telle analyse. Plus généralement, nous croyons qu'un CCFV incrémental permettrait des gains de performance significatifs, comme c'est le cas pour les solveurs de théorie. Un point de départ serait de construire sur des techniques telles que celles décrites par Moura et Bjørner [dMB07] pour effectuer un E -matching incremental dans Z3. La portée de CCFV peut être étendue en allant au-delà de la logique équationnelle du premier ordre. Pour supporter d'autres théories, les calculs doivent être augmentés avec des règles pour les nouveaux symboles interprétés. Pour gérer l'arithmétique linéaire, par exemple, CCFV devrait être capable d'effectuer l'unification modulo associativité, commutativité et identité additive). Les implémentations pratiques nécessiteront également du solveur qu'il fournisse des contrôles d'implantation efficaces en relation avec les nouveaux symboles interprétés, comme c'est le cas pour l'égalité. Si la décision est facilement perdue lors de la combinaison de théories dans une logique quantifiée, il faut trouver un bon équilibre entre les procédures de décision pour des fragments spécifiques, tels que le fragment essentiellement non interprété décrit par Ge et de Moura [GdM09], et des heuristiques efficaces pour des paramètres incomplets . Outre le raisonnement théorique, l'unification de l'ordre supérieur pourrait aussi être abordée par CCFV. Les calculs devraient tenir compte des applications partielles, des variables fonctionnelles et des abstractions lambda. Cela permettrait aux solveurs SMT de gérer de manière native les problèmes d'ordre supérieur, évitant ainsi l'exhaustivité et les problèmes de performance avec des encodages maladroits dans la logique du premier ordre. Une autre extension possible de CCFV est de gérer l'E -unification rigide, de façon à l'intégrer dans des tableaux et des techniques basées sur des calculs séquentiels tels que BREU [BR15b] ou la résolution de conflit [SP16]. Cela équivaut à avoir des égalités avec variables dans E, ce qui signifie un changement significatif de l'algorithme CCFV. Cependant, cela permettrait d'intégrer une procédure efficace axée sur les objectifs dans des calculs qui nécessitent la résolution de problèmes d'E -unification. CCFV peut être considéré comme une première étape vers un "solveur théorique" pour que les formules quantifiées soient intégrées dans un solveur CDCL(T ). Les techniques d'instanciation basées sur CCFV évalueraient le modèle candidat avec des formules quantifiées et: i) fournit un modèle fini lorsqu'il existe, ii) dérive des cas qui réfutent le candidat lorsqu'il existe, iii) propage les instanciations pertinentes et iv) est incrémental par rapport aux affectations propositionnelles. L'incrémentalité dépend de la mise en oeuvre de CCFV. L'instanciation basée sur les conflits répond déjà partiellement à (ii) et (iii), tandis que l'instanciation basée sur les triggers s'insère dans (iii) et l'instanciation basée sur le modèle quelque part dans (i) et (ii). La façon d'étendre les techniques d'instanciation afin d'atteindre pleinement ces objectifs reste un problème ouvert. Une technique complète d'instanciation basée sur le conflit, au moins par rapport à la logique équationnelle de premier ordre, pourrait être obtenue en considérant des formules quantifiées simultanément au lieu d'indépendamment, c'est-à-dire en trouvant des substitutions σ telles que

  ψ n } Les techniques des tableaux et des calculs de superposition, qui considèrent nativement des formules quantifiées simultanément, pourraient être combinées avec CCFV pour résoudre l'implication ci-dessus. Notre deuxième contribution a été d'introduire un cadre pour représenter et générer des preuves du traitement de la formule et sa mise en oeuvre dans veriT et Isabelle/HOL. Le cadre centralise la question subtile de la manipulation des variables et des substitutions liées de manière efficace. Ce cadre est suffisamment souple pour tenir compte de nombreuses transformations intéressantes. Bien qu'il ait été implémenté dans un solveur SMT, il semble qu'il n'y ait pas de limitation intrinsèque qui empêcherait son utilisation dans d'autres types de prouveurs automatiques du premier ordre ou même d'ordre supérieur. Le cadre couvre de nombreuses techniques de prétraitement et peut faire partie d'une plus grande boîte à outils. Il permet à veriT, dont les preuves détaillées ont été l'une de ses caractéristiques définissantes, de produire des justifications plus détaillées que jamais. Cependant, il existe encore des transformations globales pour lesquelles les preuves sont inexistantes ou laissent beaucoup à désirer. Pour gérer ces transformations, notre notion de contexte devrait être étendue, ainsi que les opérations autorisées à être exécutées sur des termes, de manière à pouvoir aller au-delà du remplacement de termes par leur équivalent. Le cadre peut également être étendu pour gérer différentes constructions de langage, telles que les abstractions lambda. Compte tenu de la généralité du calcul du traitement et de l'algorithme producteur de preuves, des opérations telles que la β-réduction peuvent être facilement intégrées.

  Definition 2.11 (Extending interpretations). Given two languages L and L , and an Linterpretation M = A, V , an L -interpretation M = A , V extends M if and only if (i) L ⊇ L ; (ii) every domain set in A is a subset of the respective domain set in A ; (iii) for every function symbol f interpreted in M, f I in M extends f I , i.e. f I coincides with f I on the domain sets of A An L -interpretation M extends a class of L -interpretations Ω if and only if M extends each interpretation M ∈ Ω. • Let M = A, V be an L -interpretation. The notation M xn → dn denotes an L -interpretation with the same structure as M and whose valuation V xn → dn agrees with V except for x 1 , . . . , x n , besides mapping each τ -variable x i into the element d i ∈ D τ .

  Definition 2.14 (Theory). A theory T is a set of L -sentences closed under entailment: for every L -formula ϕ, if T |= ϕ then ϕ ∈ T .•To work with the above definition in terms of interpretations, we present the following definitions. Given an L -interpretation M, the theory of M, denoted Th(M), is the set of all L -sentences satisfied by M. This notion is generalized to a class of L -interpretations Ω, such2.3. Satisfiabilitythat the theory of Ω, denoted Th(Ω), is the set of all L -sentences simultaneously satisfied by every M ∈ Ω.Definition 2.15 (Satisfiability modulo theory). Consider a theory T = Th(Ω), in which Ω is a class of L -interpretations, and a language L such that L ⊇ L . We say that an L -formulaϕ is T -satisfiable ifand only if there is an interpretation M which extends Ω and is a model for ϕ. Similarly, given L -formulas ϕ and ψ, we say that ϕ T -entails ψ, written ϕ |= T ψ, if and only if every L -model of ϕ extending Ω is also a model of ψ. •

  Definition 2.16 (Satisfiability modulo a combination of theories). An L -interpretation M is a L -reduct of an L -interpretation M , with L ⊇ L , if and only if M and M have the same frame and the interpretation function of M coincides with that of M on the symbols of L .

Figure 3

 3 Figure 3.1: An abstract procedure for checking the satisfiability of quantifier-free formulas based on the CDCL(T ) framework.

  which then triggers CheckGround to determine the T -satisfiability of the conjunctive set of literals E = {a ≤ b, b ≤ a + x, x 0, f (a) f (b)}. Generally, this would be done jointly by a congruence closure procedure [NO80, BTV03] for handling equality and uninterpreted symbols together with a simplex algorithm [DdM06] for handling arithmetic, both combined in a Nelson-Oppen framework. The arithmetic solver will determine that a and b are equal, and provide the equality a b to the congruence closure algorithm. By congruence, f (a) f (b) is derived, which is in conflict with the literal f (a) f (b) from E. Therefore E is T -unsatisfiable and the conflict clause

  Figure 3.2: An abstract procedure for checking satisfiability based on the CDCL(T ) framework.

  Given a model E ∪ Q, trigger based instantiation considers each quantified formula ∀x n . ψ in Q independently. It proceeds by 1. selecting triggers T 1 , . . . , T m from the terms in ψ 2. deriving the set of instantiation lemmas

  Example 3.2. Let E and Q be conjunctive sets, with E = {f (a) g(b), h(a) b, f (a) f (c)} and Q = {∀x. f (x) g(h(x))}. Possible triggers for ∀x. f (x) g(h(x)) are T 1 = {f (x)}, T 2 = {h(x)}, T 3 = {f (x), g(h(x))} and so on. If only T 1 is chosen, the possible instantiations for the quantified formula are derived by E -matching f (x) with terms containing f -applications in their congruence classes. The only such congruence class over T(E) is {f (a), f (c), g(b)}. Therefore the resulting substitutions are obtained from ematch(f (x), g(b), {{x → x}}). Since g(b) is congruent to the terms f (a) and f (c), this function is reduced to ematch(x, a, {{x → x}}) ∪ ematch(x, c, {{x → x}}) which yields the set of substitutions with σ 1 = {x → a} and σ 2 = {x → c}. These substitutions lead to the instantiation lemmas ∀x. f (x) g(h(x)) → f (a) g(h(a)) and ∀x. f (x) g(h(x)) → f (c) g(h(c)) which are then added to the original problem. Trigger selection The effectiveness of trigger based instantiation is highly dependent on which terms are selected to compose triggers. Therefore good selection strategies are paramount for efficient CDCL(T ) solvers. Alternatively, users may annotate quantified formulas with triggers, thus capturing their intuition of which instantiations are more important to solve a problem. The selection strategy also influences the completeness of the solver. Dross et al. [DCKP13] and Bansal et al. [BRK+15] have presented dedicated trigger selection strategies to obtain completeness for specific fragments of first-order logic, while Rümmer [Rüm12] presents a calculus, not in CDCL(T ) framework, whose completeness results are independent of the trigger selection strategy.

  goal-oriented techniques, such as the techniques based on the superposition calculus, there are no straightforward redundancy criteria for the elimination of derived instances in the CDCL(T ) framework. Therefore useless instances are generally kept, potentially hindering the solver's performance. Relying on heuristic instantiation also leads to the so called butterfly effect: small changes on the structure of the input problem have unpredictable effects on the solver's outcome. This is particularly harmful since CDCL(T ) solvers are commonly used as backends in a myriad of tools, e.g. in formal verification, which cannot afford to suffer from such instability. These issues started to be addressed by Reynolds et al.[START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF] when introducing conflict based instantiation in the context of a CDCL(T ) solver. It is a goal-oriented instantiation technique: only instances which are conflicting with the current ground model are derived. For efficiency reasons, quantified formulas are evaluated independently in the search for conflicting instances.

Example 3. 6 .

 6 Consider again the conjunctive sets E = {f (a) g(b), h(a) b, f (a) f (c)} and Q = {∀x. f (x) g(h(x))} from Example 4.2. While the trigger {f (x)} led to the two instantiation lemmas ∀x. f (x) g(h(x)) → f (a) g(h(a)) and ∀x. f (x) g(h(x)) → f (c) g(h(c)) conflict based instantiation would derive only the first lemma, since E |= f (a) g(h(a)) makes

  Example 3.7 ([Rey16]). Let E = {a c, f (b) b, g(b) a, f (a) a, h(f (a)) d, h(b) c} and consider a quantified formula ∀x. f (g(x)) h(f (x)). The instance f (g(b)) h(f (b)) is conflicting with E, since E |= f (g(b)) h(f (b)). The search for this conflicting instance is performed by deriving constraints based on the fact that E |= f (g(b)) a ∧ h(f (b)) c and E |= a c. Therefore if an assignment is provided for the variable x such that the constraints f (g(x)) f (g(b)) and h(f (x)) h(f (b)) hold then this assignment embodies a substitution leading to a conflicting instance of the quantified formula.

  Example 3.8 ([START_REF] Reynolds | Conflicts, Models and Heuristics for Quantifier Instantiation in SMT[END_REF]). If in Example 3.7 the literal a c were not present in E then the given quantified formula would not have a conflicting instance. The instancef (g(b)) h(f (b)),however, together with E would entail that a c. Therefore deriving this instance propagates an equality for the terms in E.Limitations The procedure presented by Reynolds et al. is efficient and greatly improves the instantiation module in CVC4, but no formal guarantees are given about the exact complexity of the problem it addresses or that conflicting instances for a given quantified formula will be found when they exist. A more general limitation for the search itself for conflicting instances is that accounting for theories beyond equality is particularly complicated. Remember that the search requires finding a substitution σ such that, for some theory T , E |= T ¬ψσ holds. It is thus necessary to efficiently check entailment modulo T . In a regular CDCL(T ) solver this can be done very efficiently for the theory of equality by using the data structures in place for performing the congruence closure decision procedure, but the same does not apply to other theories.Example 3.9 ([START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF]). Consider T to be a combination of the theories of equality and linear integer arithmetic. Let E = {f (a) b, g(a) ≥ b + 1} and consider the quantified formula ∀x. f (x) g(x). The substitution σ = {x → a} leads to the conflicting instance f (a) g(a).

(

  dis)unification problem as the cornerstone of this framework, in which trigger, conflict and model based instantiation techniques can be cast. This problem relates to the classic problem of rigid E -unification[START_REF] Degtyarev | What You Always Wanted to Know about Rigid E-Unification[END_REF], pervasive to sequent and tableaux based calculi for equational firstorder logic. By exploiting the similarities between CDCL(T ) and these frameworks, we build on conventional techniques to solve E -unification and present a decision procedure for E-ground (dis)unification: Congruence Closure with Free Variables (CCFV, for short), which extends the classic congruence closure algorithm[START_REF] Nelson | Fast Decision Procedures Based on Congruence Closure[END_REF][START_REF] Nieuwenhuis | Fast congruence closure and extensions[END_REF], to accommodate free variables. We then show how to build on CCFV to perform trigger, conflict and model based instantiation.A detailed accounting of the implementation and experimental evaluation of CCFV and the instantiation techniques around it is given in Chapter 5. The work described in these chapters led to a joint publication with Pascal Fontaine and Andrew Reynolds[START_REF] Barbosa | Congruence Closure with Free Variables[END_REF].

  only equations, there is a single equation in the conclusion and the removal of disequalities preserves the entailment relation, E-ground (dis)unification is shown to be an instance of rigid E -unification. Example 4.1. Consider the sets of equality literals E = {f (a) f (b), h(a) h(c), g(b) h(c)}

  2.1, a trigger T for a quantified formula ∀x n . ψ is a set of non-ground terms which collectively contain all variables bound by the quantifier, i.e. T = {u 1 , . . . , u m } such that u 1 , . . . , u m ∈ T(ψ) and {x n } ⊆ FV(u 1 )∪• • •∪FV(u m ). Instantiations are determined by Ematching all terms in T with terms in T(E), such that resulting substitutions allow instantiating ∀x n . ψ into ground formulas. Computing such substitutions amounts to solving the E-ground (dis)unification problem

Example 4. 2 .

 2 Consider the conjunctive sets E = {f (a) g(b), h(a) b, f (a) f (c)} and

  which is solved by the substitutions σ 1 = {y → f (a), x → a} and σ 2 = {y → f (c), x → c} By considering the part of the solutions that range over x, the instantiation lemmas generated would be, as in Example 4.2, ∀x. f (x) g(h(x)) → f (a) g(h(a)) (4.1) and ∀x. f (x) g(h(x)) → f (c) g(h(c)) (4.2) -E |= (h(x) y)σ, solved by σ = {y → h(a), x → a}, yielding only the instantiation lemma 4.1.

  Finding a conflicting instance amounts to solving the E-ground (dis)unification problem E |= ¬ψσ, for some ∀x n . ψ ∈ Q since ¬ψ is a conjunction of equality literals. Example 4.3. Let E and Q be as in Example 4.2. Finding conflicting instances corresponds to solving the problem E |= (f (x) g(h(x))) σ whose unique solution is σ = {x → a}. It leads to the instantiation lemma ∀x. f (x) h(g(x)) → f (a) h(g(a)) which forces the derivation of a new candidate model E ∪ Q.

  For simplicity, the extension E tot is shown explicitly only for ∀x. f (x) g(x),E tot = E ∪ {a b, a f (a), b f (a)} ∪ {f (b) f (a), f (f (a)) f (a), g(a) a, g(f (a)) a} ∪ {. . . } Solving the E-ground (dis)unification {. . . , f (a) g(b), f (b) f (a), . . . } |= f (x) g(x)σ leads to the solution σ = {x → b}, from which the instantiation lemma

  is replaced by rep({x s}, C), one variable (either x, or s, if it is a variable, depending on the representative chosen) disappears from the right side. The other rules can be divided into two categories. The branching rules (Uvar through Dgen) enumerate all possibilities for deriving the entailment of some literal from C. The rules are based on the entailment conditions from Theorem 4.4. Condition (1) is represented by rule Assign. Condition (2) by rule Uvar. Condition (3) by rule Assign. Condition (4b) is represented by rules Ucomp and Ugen, with the first also accounting for condition (4a). Condition (5) is handled by rules Dvar, Dfapp and Dgen, which restrict the terms to consider according to the structure of the constraint.

1.

  Select branch: While C is a disjunction, apply Split and consider the leftmost branch, by 4.2. Calculus convention. 2. Simplify constraint: Apply the rule for which sel(C) is amenable. 3. Discard failure: If Fail was applied or a branching rule had the empty disjunction as a result, discard this branch and consider the next open branch. 4. Mark success: If the right hand side has been reduced to , all remaining constraints in the branch are entailed by E ∪ E σ . Mark the branch as successful and then consider the next open branch. A solution σ for the E-ground (dis)unification problem E |= Lσ can be extracted at each successful branch. Example 4.7. Consider again the sets E = {f (a) f (b), h(a) h(c), g(b) h(c)} and

  }, {g(b)}} with the disequalities entailed by E being g(b) h(c) and g(b) h(a).

  d(C) be the sum of the depths of all occurrences of variables in the literals of the conjunction C. The Assign rule decreases the number of variables of C. The Fail rule closes a branch. The Yield removes constraints, of which there are only finitely many. All remaining rules decrease d in the transition from E σ E C to E σ E C 1 ∨ • • • ∨ C n , i.e. d(C) > d(C 1 ), . . . , d(C) > d(C n ). At each node, d(C) or the number of variables in C are decreasing, except at the Split, Fail or Yield steps. Since no branch can contain infinite sequences of these applications, the depth of the any derivation tree is always finite.

Case Split:

  Follows by entailing a disjunct implying the entailment of the disjunction. Case Assign: Let C = C 1 ∪ {x s}. Again, C is the result of replacing a variable in C 1 according to the assignment x s being added to the current partial solution. Since σ stems from a successful branch deriving from C , it maps x and s to a ground term congruent to the representative they were replaced by in C 1 . Therefore, from E |= C σ it follows that E |= C 1 σ. Moreover, trivially E |= {xσ sσ}. Thus E |= Cσ.

  {x 1 a, x 2 a, x 3 b} E which has the same solutions as in Example 4.7.

E

  -ground (dis)unification problem. An experimental evaluation measures the impact of optimizations and instantiation techniques based on CCFV in veriT and CVC4. Comparisons are shown with previous versions and with the instantiation based SMT solver Z3 [dMB08b]. Limitations Efficient implementations of the congruence closure decision procedure are currently guaranteed to be closed under entailment only for congruent terms, not for disequal ones. E.g. g(f (a), h(b)) g(f (b), h(a)) ∈ E does not lead to the addition of a b to the data structure. A complete implementation of CCFV requires the derivation of all entailed disequalities from E. Therefore for now we implement incomplete versions of the rules Dvar, Dfapp, and

Figure 5

 5 Figure 5.1: Backtracking CCFV algorithm

  Figure 5.3: Improvements in veriT and CVC4

Figure 5

 5 Figure 5.4: Depth-first versus breadth-first CCFV

  Reflx → a x aRefl x → a x a Cong x → a p(x, x) p(a, a) Let (let x a in p(x, x)) p(a, a)It is also possible to further process the substituted term, as in this derivation:Taut + a + 0 a . . . Cong x → a p(x, x) p(a, a) Let (let x a + 0 in p(x, x)) p(a, a)Example 6.2. The following derivation tree, in which ε x abbreviates εx. ¬ p(x), justifies the skolemization of the quantifier in the formula ¬ ∀x. p(x):Refl x → ε x x ε x Cong x → ε x p(x) p(ε x ) Sko ∀ (∀x. p(x)) p(ε x ) Cong (¬ ∀x. p(x)) ¬ p(ε x )

  Example 6.3. The next derivation tree illustrates the interplay between the theory rule Taut T and the equality rules Trans and Cong:1×0 < k) (k < k)We could extend the tree at the bottom with an extra application of Trans and Taut < to simplify k < k further to false. The example demonstrates that theories can be arbitrarily finegrained, which often makes proof checking easier. At the other extreme, we could have derived(k + 1×0 < k) false using a single Taut + ∪ × ∪ < inference.Example 6.4. The tree below illustrates what can go wrong if we ignore side conditions:Refl Γ 1 f(x) f(x) Refl Γ 2 x f(x) Refl Γ 3 p(y) p(f(f(x))) Let* Γ 2 (let y x in p(y)) p(f(f(x))) Let Γ 1 (let x f(x) in let y x in p(y)) p(f(f(x)))Bind (∀x. let x f(x) in let y x in p(y)) (∀x. p(f(f(x))))

Refl Γ 1

 1 f(x) f(z) Refl Γ 2 x f(z) Refl Γ 3 p(y) p(f(z)) Let Γ 2 (let y x in p(y)) p(f(z)) Let Γ 1 (let x f(x) in let y x in p(y)) p(f(z)) Bind (∀x. let x f(x) in let y x in p(y)) (∀z. p(f(z)))

  The incrementality depends on the implementation of CCFV. Conflict based instantiation partially achieves (ii) and (iii), while trigger based instantiation fits into (iii) and model based instantiation somewhat into (i) and (ii). How to extend the instantiation techniques in order to fully accomplish these goals remains an open problem. A complete conflict based instantiation technique, at least with relation to equational first-order logic, could be achieved by considering quantified formulas simultaneously instead of independently, i.e. finding substitutions σ such that E |= ¬ψ 1 σ ∨ • • • ∨ ¬ψ m σ, with Q = {∀x n 1 . ψ 1 , . . . , ∀x nm . ψ m }

  and only if ϕ M x →d = , for every d ∈ D τ , x being a τ -term;

	⊥ otherwise.

A formula ψ is true in M if and only if ψ M = and false in M if and only if ψ M = ⊥. •

2.3 Satisfiability

Definition 2.13 (Satisfiability). Given an L -interpretation M and an L -formula ψ, M satisfies ψ, written M |= ψ, if and only if it makes it true, i.e. ψ M = . A formula ϕ is satisfiable if and only if there is an interpretation M such that M |= ϕ, in which case we say that M is a model of ϕ; otherwise ϕ is unsatisfiable, written |= ¬ϕ. Given two L -formulas ϕ and ψ, ϕ entails ψ, written ϕ |= ψ, if and only if every model of ϕ is also a model of ψ. An L -formula ϕ is valid, written |= ϕ, if and only if it is true in every L -interpretation M.

•

  for comprehensive overviews). It originated with the simpler problem of Boolean satisfiability, i.e. determining if a propositional formula has a model. This problem is commonly known as SAT, and is one of the first to be shown NP-complete. As such it was an intractable problem for many years, until the so called SAT revolution in the

	turn of the last century: modern SAT solvers, implementing the conflict-driven clause-learning
	(CDCL) calculus, can efficiently solve very large problems coming from real world problems
	containing hundreds of thousands of propositional variables and millions of clauses. SMT solving
	developed initially in the 1970s and 1980s by pioneers such as Nelson and Oppen [NO79, NO80]

  Triggerheads are terms with at least one of the quantified variables as subterm, and that do not include trigger killers. Trigger killers are terms not permitted to appear in triggers, typically applications of interpreted symbols, e.g. arithmetic operations or logical connectives.2. Candidate triggers are built by combining all possible trigger heads while ensuring two properties: adequacy and parsimony. A candidate is adequate if it contains all the quantified variables and parsimonious if removing any term from the candidate makes it inadequate.

E.g. a quantified formula ∀x. p 1 (x) ∨ • • • ∨ p n (x) has the trigger heads {p 1 (x), . . . , p n (x)} and 2 n adequate candidates, but only n which are parsimonious: the singletons {p 1 (x)}, . . . , {p n (x)}.

  Model based quantifier instantiation (MBQI) is a complete instantiation technique for CDCL(T )solvers introduced by Ge and de Moura[START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF]. It attempts to build a model for E ∪ Q by systematically creating candidate interpretations M which satisfy E and evaluating whether they also satisfy Q. The former is guaranteed by construction. The latter is checked, for each quantified formula ∀x n . ψ ∈ Q, by looking for instances ¬ψσ which are T -satisfied by M, i.e.whether M |= T ¬ψσ holds, given a background theory T . If no such instance exists, then M satisfies E ∪ Q. Otherwise each of these instances is a witness of why M is not a suitable candidate. They are added to the original problem with instantiation lemmas, thus removing this candidate from consideration in the following iterations. The successive rounds of instantiation either lead to unsatisfiability or, when no conflicting instance is generated, to satisfiability with a concrete model. Ge and de Moura present several fragments of first-order logic in which MBQI is complete, including fragments containing arithmetic.

	Example 3.11

  . Since congruence classes are sets, function applications whose arguments are congruent have the same signature. If e.g. a and b are equal, then f (a) and f (b) have the same signature. The signature class of t is a set [t] E containing one and only one term in the congruence class of t for each signature. Considering again the previous example, since f (a) and f (b) have the same signature, only one of them would be in their signature class. Notice that the signature class of two terms in the same congruence class is the same set of terms, and is a subset of their congruence class. We drop the subscript in [t] E when E is clear from the context. The set of signature classes of E on a set of terms T is E cc = {[t] | t ∈ T}. We may overload the above notations when E is a set of equality literals, not only of equalities. In this case we consider the congruence closure with relation to the equalities in E.

	We fix the entailment relation |= to represent entailment modulo ground equational reasoning,

Given a set of ground terms T closed under the subterm relation and a congruence relation on T, a congruence over T is a subset of {s t | s, t ∈ T} closed under entailment. The congruence closure (CC, for short) of a set of equations E on a set of terms T is the least congruence on T containing E. Given a consistent set of equality literals E, two terms t 1 , t 2 are said to be congruent iff E |= t 1 t 2 and disequal iff E |= t 1 t 2 . The congruence class in T of a given term is the set of terms in T congruent to it. The signature of a term is the term itself for a nullary symbol, and f (c 1 , . . . c n ) for a term f (t 1 , . . . t n ), with c i being the congruence class of t i i.e. given a set of ground equality literals E and ground terms s and t, 1. E |= s t if and only if [s] E = [t] E , and 2. E |= s t if and only if there is a disequality s t or t s in the set E , which is the closure of E with relation to disequalities, such that [s]

  This is obviously true for full edges, since variables are not linked to any term in G. Consider the earliest (according to the dependency order of congruence edges) congruence edge between f (t 1 , . . . , t n ) and f (t 1 , . . . , t n ) contradicting this hypothesis. Then there is a path from f (t 1 , . . . , t n ) to a ground term; this path cannot contain full edges, because this would involve two edges with a variable. Hence the path only contain congruence edges and t 1 , . . . t n are all equal to ground terms. The same holds for f (t 1 , . . . , t n ), then t i and t i are both linked to ground terms, for i ∈ {1, . . . n}. One new earlier edge contradicts the hypothesis too.As a corollary of the previous paragraph, given two terms t, t , if both terms are ground, Otherwise if S x contains a term in u ∈ T(L), for all variables y in S x , yσ = u. If S x does not contain any term in T(E ∪ L), a variable z in S x is chosen, and for all variables y in S x , yσ = z. Trivially, ran(σ ) ⊆ T(E ∪ L). we prove that E ∪ E σ |= L if and only if E ∪ E σ |= L, or further, that for any two termst, t in T(E ∪ L), E ∪ E σ |= t t if and only if E ∪ E σ |= t t . Since E ∪ E σ |= E ∪ E σ , the only non trivial direction is that, if E ∪ E σ |= t t , E ∪ E σ |= t t. This has already be proven in the case of two ground terms. By construction σ and σ induce the same partition on the variables, so this is true also if t and t are two variables. If there is a path between t and t with only congruence edges in the graph for E ∪ E σ , t and t are still congruent according to E ∪ E σ , thanks to the fact that equality between variables and equality between ground terms is preserved. As a corollary, any equality between terms in T(E ∪ L) is preserved.

	Now

in which σ is a substitution and t is a term. Note that E |= Lσ holds if and only if E ∪ E σ |= L also does.

To compute the congruence closure of a set of equations E on a set of terms T, it suffices to compute a congruence graph on T. Two terms t, t are equal according to E if and only if there is a path between them in the graph. There is a full edge in the graph between two terms in any equation of E, and there is a congruence edge between two terms such that all arguments are pairwise equal (i.e., there is a path between them). Some (congruence or full) redundant edges can be omitted if the extremities are already connected. The congruence graph is a least fixed point, so the explanation for the existence of a congruence edge can always be traced back to full edges only. Congruence edges can be ordered by their dependency.

Consider a congruence graph G induced by E on terms T(E ∪ L ∪ E σ ), and a congruence graph G induced by furthermore adding edges for σ. Besides the edges corresponding to σ, that is, edges with a variable, the only additional edges are congruence edges; we assume no redundant edge is added to G . Variables are at most linked to one term, and by a full edge.

Other non-variable free term can only be linked either by a full edge to a variable, or to a term by a congruence edge.

All edges in G \ G involve at least one term u that is not (directly or indirectly) linked to any ground term in G.

E ∪ E σ |= t t if and only if E |= t t .

In the following, we build an acyclic substitution σ such that ran(σ ) ⊆ T(E ∪ L), and for

two terms t 1 , t 2 ∈ T(E ∪ L), E ∪ E σ |= t 1 t 2 if and only if E ∪ E σ |= t 1 t 2 . Grounding σ is again trivial. For each variable x in dom(σ), if S x contains a ground term t in T(E ∪ L), then xσ = t.

The substitution σ is acyclic. Otherwise for some n, E ∪ E σ |= x i f i (. . . , x (i+1) mod n , . . . ) (i ∈ {1, . . . n}) and also, since σ is ground,

  1: Condition (1a) states that xσ and yσ are the same term, while (1b) that they are (possibly different) congruent terms. Each implies that the entailment holds. If E |= σ and both (1a) and (1b) fail, then xσ and yσ are not congruent terms, which is a contradiction.Case 2: the side condition implies the entailment. If E |= σ, and since x occurs in f (s 1 , . . . , s n ), then xσ and f (s 1 , . . . , s n )σ are different terms occurring in the same congruence class. This class must contain both a term t and a term f (t 1 , . . . , t n ) on which the former is congruent to a subterm of the latter. This can only be the case if both t and f (t 1 , . . . , t n ) occur in E.Case 3: Similarly to 1, both conditions imply that the entailment holds and it holding while the conditions do not is a contradiction. The conditions are independent of x occurring on f (s 1 , . . . , s n ), since (3b) does not restrict the ground terms t 1 , t 2 .Case 4: By congruence, if condition (4a) holds then the function applications are congruent, while (4b) directly implies they are. If E |= σ and since it is not possible for two different function

applications not in T(E) to be congruent, then f = g and f (u 1 , . . . , u n )σ and g(v 1 , . . . , v n )σ are the same function application over congruent arguments, or f (u 1 , . . . , u n )σ and g(v 1 , . . . , v n )σ are ground terms occurring in E and in the same congruence class in E cc .

Case 5: Since two terms not in T(E) cannot be entailed disequal unless they are congruent to two terms in T(E) which are disequal, E |= σ holds if and only if uσ and vσ are in the congruence classes of disequal terms occurring in E.

Note that in cases (1), (

3

) and (4a) the entailment does not necessarily depend on E, i.e. a solution that make the terms syntactically equal is possible. The other cases, however, can only be entailed if there are certain terms in E into which the non-ground terms can be made equal to by the substitution. Example 4.5. Considering again E and L as in Example 4.1, the calculus should find a substitution σ such that

  σ g is ground, and E |= Lσ g .Given an E-ground (dis)unification problem E |= Lσ, the CCFV calculus computes the various possible E σ corresponding to a coverage of all substitution solutions, i.e. such that E ∪ E σ |= L, whose range is in T(E ∪ L). We describe the calculus as a set of rules that operate on states of the form E σ E C, in which C is a formula stemming from the decomposition of L into an AND-OR combination of simpler constraints, and E σ is a conjunctive set of equalities representing a partial solution for a given combination. Starting from the initial state E L the right hand side of the state is progressively decomposed, whereas the left side is step by step augmented with new equalities building the candidate solution. represents an empty conjunctive set. Moreover, as the partial solution is built the remaining constraints are updated to reflect the current assignments of variables, therefore searching only for further solutions which are compatible with the current one. Example 4.5 shows that, for a literal to be entailed by E ∪ E σ , sometimes several solutions E σ exist, thus the calculus involves branching.

  s 1 ), . . . , rep(E σ , s n )) otherwise and write rep(E σ , C) to denote the result of applying rep according to E ∪ E σ on both sides of

	each literal s	s or s	s in C. The above definition of rep leaves room for some choice of
	representative, but soundness and completeness are not impacted by the choice. What actually

matters is whether the representative is a variable, a ground term or a non-ground function application. The Assign rule adds equations from the right side of the state into the tentative solution in the left side of the state: it extends E σ with the mapping for a variable. Because C

4.2. Calculus

  This can be checked straightforwardly by determining whether Yield is applicable in a state E σ E rep(E σ , ).

Example 4.8. Let E ∪ Q be such that E |= p(c, d) and Q has a quantified formula ∀xy. ψ containing a literal p(x, y). If an instantiation σ = {x → c, y → d} is derived for ∀xy. ψ, it can be quickly determined that, since E |= p(x, y)σ , this instantiation should be discarded.

Table 4 .

 4 2: Non-backtracking CCFV calculus. E is fixed from a problem E |= Lσ.Example 4.10. Consider the application of Meet on the state {{x f (y)}} E g(z) t {{x y, z t}} E simple derivation strategy for this new CCFV calculus is to decompose the entailment problems until they depend only on variable assignments and ground reasoning, and then combine the found solutions accordingly. Given an initial state { } E L, branching rules and splitting rules are applied exhaustively, until all solving statements have the form { } E A ∧ C, in which A and C are conjunctive sets of variable equations and of ground constraints, respectively. By applying a series of Assign and Yield ∧ or Fail ∧ rules, each solving statement will become either Σ E , if the assignments in A are compatible and E entails C, or ∅ E ⊥, otherwise. The resulting solving statements are successively combined and simplified with series of applications of Join and Meet, and both cases of Yield and Fail. One obtains either a state ∅ E ⊥, if the solutions are not compatible, or a state Σ E , otherwise. In the latter case all solutions in Σ are solutions for the E-ground (dis)unification problem. Example 4.11. Consider again E, L, and E cc as in Example 4.7:

	Since both sets of solutions are singletons, there is only one case to consider. Let {x	f (y)}
	be the solution chosen for the normalisation. The representatives of the variable x, y, z in it are
	f (y), y, and z, respectively. Thus the resulting state is
	{{x f (y)}} E g(z) t ∧ f (y) y ∧ z t ∧
	with the normalisation of the solution and the constraint from the combined state. This shows
	that the two solutions are compatible only if f (y)	y can be solved, since x was assigned in
	both solutions.
	4.3.1 Strategy

A

  Top symbol indexing of E cc The set of signature classes E cc , as defined in Chapter 4, is indexed by top symbols. The index consists of entries of the form (t m1 , . . . , t mn ) in which f is a function symbol of arity n and each function application f (t i1 , . . . , t in ) is a term occurring in E cc .We define below several operations based on this index and on the E-graph that are used in the E-ground (dis)unification solving.4 Let f be a function symbol and s a term:class(s): yields the set of terms in the signature class of s, i.e. all terms occurring in [s] from E cc . These results can be directly retrieved from the E-graph in constant time.find(s): yields the representative of class(s), i.e. a distinguished term from the signature class of s in E cc . Also directly retrievable from the E-graph in constant time.This operation is what allows the efficient checking of whether two ground terms t 1 and t 2 are congruent. If they both occur in the E-graph, it suffices to check whether it holds that find(t 1 ) = find(t 2 ), i.e. whether the DAG representation of both representatives is syntactically equal. Otherwise it is necessary to check if the terms have the same top symbol and if arguments of matching position are congruent.

	f →	   	f (t 11 , . . . , t 1n ) . . .
		  

f

  unify argumentsSols ← Sols ∪ CCFV(E σ , C ∪ {u 1 u 1 , . . . , u n u n }) for t ∈ reps(f ) do // E -matching into same class Sols ← Sols ∪ CCFV(E σ , C ∪ {f (ū n ) t, g(ū n ) t})

	return Sols
	x t :
	for t ∈ diseqs(t) do	// Assignment into a disequal term
	Sols ← Sols ∪ CCFV(E σ , C ∪ {x t })
	return Sols
	f (ū n ) t :	// E -matching into a disequal term
	for t ∈ diseqs(t) do
	Sols ← Sols ∪ CCFV(E σ , C ∪ {f (ū n ) t })
	return Sols
	x f (ū n ) :	// Dfapp
	for t ∈ reps(f ) do
	Sols ← Sols ∪ CCFV(E σ , C ∪ {f (ū n ) t, x t})
	return Sols
	f (ū n ) g(ū n ) : for t ∈ reps(f ) do	// E -matching into disequal terms
	Sols ← Sols ∪ CCFV(E σ , C ∪ {f (ū n ) t, g(ū n ) t})
	return Sols
	x y :	// Dvar
	for each signature t in E cc do
	for t ∈ diseqs(t) do
	Sols ← Sols ∪ CCFV(E σ , C ∪ {x t, y t })
	return Sols

  . . , w n ), in which each w i is either a ground term or a nullary symbol * , and yield all terms f (t 1 , . . . , t n ) in E cc such that, at each position i ∈ {1..n} in which w i = * , E |= t i w i . In the example above, the query would be whether apps(f, g(t), * ) is empty. The operation apps(f, w 1 , . . . , w n ) can be implemented by building a forest in which each tree has as root a function symbol, each edge is annotated with a term, and whose leafs are the applications of that symbol in E cc whose arguments are the annotations in the edges leading to that leaf, in the respective order. Alternatively the hash table kept internally for efficiently manipulating the E-graph could be used. This would require adding 2 n entries for each function symbol into the table, in which n is the arity of the respective function symbol. Therefore it is necessary to carefully analyse which function symbols can benefit from this check.

  Moskal et al. [MŁK08] have a somewhat similar approach for their E -matching algorithm in which sets of partial solutions need to be combined. By representing these sets as ordered trees they are able to efficiently implement combination operations. We would need to extend such data structures for our more complex solution representations, since we may have variables associated with other variables or non-ground terms, rather than only with ground terms. Consider again E, L and E cc as in Example 5.2 and assume that all the indexing operations from Section 5.1 are available. The execution of the CCFV-breadth algorithm would start with CCFV(L). Let h(x 1 )

	for it. Example 5.4.
		Dvar
	for each signature t in E cc do
	for t ∈ diseqs(t) do
	c-sols ← c-sols CCFV({x t, y t })
	Sols ← Sols c-sols	// Merge solutions from constraint
	return Sols	// Yield found solutions
	Figure 5.2: Breadth-first CCFV algorithm

Table 5

 5

	Logic	Class	Z3 cvc+d cvc+e cvc verit+tc verit+tcb verit+t verit
	UF	grasshopper sledgehammer 1249 418	411 1438 1456 1428 420 415	430 1277	435 1278	418 1134
	UFIDL all	62	62	62 62	58	58	58
		boogie	852	844	834 801	706	690	660
		sexpr	26	12	11 11	7	7	5
	UFLIA	grasshopper	341	322	326 319	356	361	340
		sledgehammer 1581	1944 1953 1929	1790	1799	1620
		simplify	831	766	706 705	803	801	735
		simplify2	2337	2330 2292 2286	2307	2303	2291
		Total	7697	8129 8060 7956	7734	7736	7261

.1: Instantiation based SMT solvers on SMT-LIB benchmarks

  The notation t[x n ] stands for a term that may depend on distinct variables xn ; t[s n ] is the corresponding term where the terms sn are simultaneously substituted for xn ; bound variables in t are renamed to avoid capture. Following these conventions, Hilbert choice and 'let' are characterized by

  tables below indicate the number of benchmark problems solved by each configuration for the quantifier-free and non-quantifier-free benchmarks:

		Without proofs	With proofs
	QF	Old code New code Old code New code
	Basic	13 489	13 496	13 360	13 352
	Extended	13 539	13 537	N/A	13 414
	Complete	13 826	13 819	N/A	N/A
		Without proofs	With proofs
	Non-QF	Old code New code Old code New code
	Basic	28 746	28 762	28 744	28 766
	Extended	28 785	28 852	N/A	28 857
	Complete	28 759	28 794	N/A	N/A

Nous avons mis l'accent ici sur la production de preuves détaillées, visant à garantir une vérification d'une complexité raisonnable et facilitant ainsi l'implémentation effective des correcteurs.Une direction prometteuse est également de reconstruire les preuves détaillées dans les assistants xxii de preuve, qui fournissent des preuves officielles fiables et vérifiées par machine des théorèmes.Un défi général consiste à effectuer dans les assistants de preuve le raisonnement nécessaire pour vérifier les preuves. Pour certaines théories, telles que l'arithmétique non linéaire, cela peut être très difficile. Cependant, une fois possible, la reconstitution complète des preuves dans des assistants de preuve augmenterait considérablement la confiance globale sur les résultats des solveurs automatiques, évitant ainsi la nécessité de faire confiance à un logiciel dont la correction repose principalement sur des tests.En conclusion, nous croyons que nos contributions sont bénéfiques pour l'état de l'art de la résolution SMT (et par conséquent aussi pour la démonstration automatique au premier ordre).En outre, étant donné que les deux cadres présentés sont assez généraux et extensibles, nous nous attendons à ce qu'ils servent de point de départ pour plusieurs autres techniques d'instanciation et de production de preuve en SMT, aidant ainsi les solveurs à résoudre des problèmes toujours plus expressifs et à produire des résultats plus fiables.

This theory coincides with many-sorted first-order logic with equality. In an SMT context the term "uninterpreted" refers to function symbols not interpreted by the background theories. Since in many-sorted equational first-order logic only the connectives and the equality symbol have fixed interpretations, all other function symbols are considered "uninterpreted".

These are sometimes also referred to as eager and lazy approaches.

This is not a requirement for handling quantified formulas in CDCL(T ), but we adopt it for simplicity, without loss of generality.

This presentation is inspired by the presentation of the indexing techniques used for E -matching by de Moura and Bjørner[START_REF] De | Efficient E-Matching for SMT Solvers[END_REF].

As of 2016.

http://isabelle.in.tum.de/repos/isabelle/file/00731700e54f/src/HOL/ex/veriT_Preprocessing. thy

Acknowledgments

Conflict based instantiation CCFV can be applied directly in the search for conflicting instances for E ∪ Q. The negation of each quantified formula in Q comprises a conjunction L of equality literals for which a solution within the context E is searched for, starting on the initial state ∅ E L. Differently from the algorithm given by Reynolds et al. [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF], CCFV finds all conflicting instantiations for a given quantified formula by being a decision procedure for the corresponding E-ground (dis)unification problem E |= Lσ.

Propagating equalities As discussed in Section 3.2.2, even when the search for conflicting instances fails it is still possible to propagate relevant equalities. Let us consider how to propagate these equalities with CCFV. Given some ¬ψ = 1 ∧ • • • ∧ n , let σ be a ground substitution such that E |= 1 σ ∧ • • • ∧ k-1 σ and all remaining literals k σ, . . . , n σ not entailed are ground disequalities with (T( k σ) ∪ • • • ∪ T( n σ)) ⊆ T(E). The instantiation ∀x n . ψ → ψσ introduces a disjunction of equalities constraining T(E). CCFV can generate such propagating substitutions if the side conditions of Fail and Yield are relaxed w.r.t. ground disequalities whose terms occur in T(E) and originally had variables: the former is not applied based on them and the latter is.

Example 4.9. Consider the conjunctive set E = {f (a) t, t g(a)} and a quantified formula ∀x. f (x) t ∨ f (x) g(x). When applying CCFV in the problem

to entail the first literal a candidate solution E σ = {x a} is produced. The second literal would then be normalized to f (a) g(a), which would lead to the application of Fail, since it is not entailed by E. However, as it is a disequality whose terms are in T(E) and originally had variables, instead the rule Yield is applied. The resulting substitution σ = {x → a} leads to propagating the equality f (a) g(a), which merges two classes previously different in E cc .

MBQI CCFV can be applied directly in the search for conflicting instances for E tot ∪ Q.

However, it is not necessary to explicitly build E tot , which can be quite large. The search can be performed on E and when a solution is not found, "definitions" for new terms can be added lazily to E tot as they are required by CCFV for building potential solutions. Differently from the model based approaches of Ge and de Moura [START_REF] Ge | Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories[END_REF] and Reynolds et al. [START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF], which allow integration of theories beyond equality, CCFV for now only handles the equational case.

A non-backtracking CCFV

The calculus in Table 4.1 is inherently backtracking because it considers one solution at a time. This is the case since conjunctive constraints can only be solved by building solutions extending a current one. In this section we present an alternative calculus for CCFV that searches for We assume that all the indexing operations from Section 5.1 are available. The execution of the CCFV algorithm would start with CCFV( , L). To ease the presentation, let us follow the selection order used in Example 4.7. First the literal h(x 1 ) h(c) is selected from the set of constraints. Its pattern matching leads to an E -matching scenario, in which the arguments of h(x 1 ) will be E -matched with the arguments of each term in apps(h, h(c)), i.e. each h-applications in class(h(c)). Let h(a) be the first of these terms. As a consequence, the following call will be with CCFV( , (L \ {h(x 1 ) h(c)}) ∪ {x 1 a}). By proceeding analogously and following the same selection criteria from Example 4.7, the CCFV algorithm will not only find the same solutions (which, is worth noting, would all be found, independently from the selection strategy) but create "break-points", i.e. recursive calls to CCFV from within loops, in the same points that the derivation tree branches, in the same order.

Ordering constraints

The CCFV algorithm, as the calculus it implements, allows any arbitrary order for selecting literals in constraints. A possible selection heuristic is to order constraints according to their "branching potential": select first the constraints whose entailment check requires less branching. This number depends on the structure of the terms in the constraint literal and on E cc , and can be approximated with different levels of precision (number of branches generated after applying one rule on the literal, number of branches after two rules, on the literal and in the results, etc.). The trade-off between classifying constraints and the gain from such classification should be taken into account. The first literals to be selected would be those whose entailment check does not require branching, i.e. equalities between syntactically equal terms, ground equalities between terms known by the E-graph or whose function symbols are different.

Discarding unsuitable branches Matching a term f (ū n ) with a ground term f ( tn ) fails unless all their ground arguments of matching position are congruent. Therefore, after an assignment and the subsequent update of the E-graph, if an argument of a term f (ū n ) occurring in one of the remaining constraints becomes ground, it can be checked whether there is a ground term f ( tn ) ∈ T(E) such that, for every ground argument u i , E |= u i t i , i.e. find(u i ) = find(t i ).

If no such term exists and f (ū n ) is not in a literal compatible with a Ucomp scenario, the whole "branch" can be eagerly discarded.

Example 5.3. Considering the CCFV calculus, in a state

Conflict based instantiation

To apply conflict based instantiation it suffices to have an outer loop that produces the conjunctive negation of a quantified formula's body, which compose a set of constraints to be directly solved by CCFV. One point to consider is which instances to generate from the found solutions to the E-ground (dis)unification problem. One conflicting instance is sufficient to rule out the current assignment E ∪Q, and this is indeed the strategy used in CVC4, the first SMT solver to use conflict based instantiation. In veriT, however, instantiating the quantified formulas with all found conflicting substitutions has been, so far, more effective than generating the minimal amount of conflicting instances.

Experiments

Here we evaluate the impact of optimizations and instantiation techniques based on CCFV. We make comparisons with previous versions of the SMT solvers veriT and CVC4, as well as with the state-of-the-art instantiation based solver Z3 [START_REF] Mendonça De Moura | Z3: An Efficient SMT Solver[END_REF]. Different configurations are identified in this section according to which techniques and algorithms they have activated:

t : trigger instantiation through CCFV (see "Trigger based instantiation" in Section 5.2.2); c : conflict based instantiation through CCFV (see "Conflict based instantiation" in Section 5.2.2);

Soundness

Lemma 6.1. If the judgment M N is derivable using the encoded inference system with the theories T 1 , . . . , T n , then

Proof. By structural induction on the derivation of M N . For each inference rule, we assume that |= T reify(M i N i ) holds for each judgment M i N i in the antecedent and show that |= T reify(M N ). Most of the cases implicitly depend on basic properties of the λ-calculus to reason about reify.

Case Taut T : Trivial because T ⊆ T by definition of T.

Cases Trans, Cong, and Bind: These follow from the theory of equality ( ).

Cases Sko ∃ , Sko ∀ , and Let: These follow from (ε 1 ) and (ε 2 ) or (let) and from the congruence of equality.

where

The L function encodes the substitution entries of Γ as λ-abstractions applied to tuples. Reducing the applied λ-abstractions effectively applies subst(Γ). For example:

For any derivable judgment Γ t u, the terms t and u must have the same sort, and the metaterms L(Γ) [ where ( * * ) is the property that ρ • subst(Γ) = subst(x n → sn , Γ) for all xn , sn , and Γ, which is easy to prove by structural induction on Γ.

Lemma 6.3. If the judgment Γ t u is derivable using the original inference system, then

is derivable using the encoded inference system.

Proof. By structural induction on the derivation of Γ t u.

Case Taut T : We have |= T Γ(t) u. Using Lemma 6.2, we can easily show that

), the side condition of the encoded Taut T rule.

Case Bind: Case Let: Similar to Trans.

Incidentally, the converse of Lemma 6.3 does not hold, since the encoded inference rules allow metaterms that contain applied λ-abstractions on the right-hand side of .

A proof of concept checker

Theorem 6.4 (Soundness of Inferences). If the judgment Γ t u is derivable using the original inference system with the theories T 1 , . . . , T n , then the entailment |= T Γ(t) u holds,

Proof. This follows from Lemmas 6.1 and 6.3. The equivalence of |= T Γ(t) u and

can be established along the lines of case Taut T of Lemma 6.3.

A proof of concept checker

We developed a prototypical proof checker for the inference system above using Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-Order Logic[END_REF], to convince ourselves that proofs generated according to it can easily be reconstructed.

The Isabelle/HOL proof assistant is based on classical higher-order logic (HOL) [START_REF]Introduction to HOL: A Theorem Proving Environment for Higher Order Logic[END_REF], a variant of the simply typed λ-calculus. Thanks to the availability of λ-terms, we could follow the lines of the encoded inference system of Sect. 6.2 to represent judgments in HOL. The proof checker is included in the development version of Isabelle. 6

Derivations are represented by a recursive datatype in Standard ML, Isabelle's primary implementation language. A derivation is a tree whose nodes are labeled by rule names. Rule

Taut T additionally carries a theorem that represents the oracle |= T , and rules Trans and Let are labeled with the terms that occur only in the antecedent (t and sn ). Terms and metaterms are translated to HOL terms, and judgments M N are translated to HOL equalities t u,

where t and u are HOL terms. Uncurried λ-applications are encoded using a polymorphic combinator case × : (α → β → γ) → α × β → γ; in Isabelle/HOL, λ(x, y). t is syntactic sugar for case × (λx.λy. t). This scheme is iterated to support n-tuples, represented by nested pairs

To implement the inference rules, it is necessary to be able to locate any metaterm's box.

There is an easy criterion: Translated metaterms are of the form (λ. . . .) . . . or case × . . . , which is impossible for a translated term. Because reconstruction is not verified, there are no guarantees that it will always succeed, but when it does, the result is certified by Isabelle's LCF-style inference kernel [START_REF] Michael | Edinburgh LCF: A Mechanised Logic of Computation[END_REF]. We hard-coded a few dozen examples to test different cases, such as this one: Given the HOL terms t = ¬ ∀x. p ∧ ∃x. ∀x. q x x and u = ¬ ∀x. p ∧ ∃x. q (εx. ¬ q x x) (εx. ¬ q x x)

and the ML tree

Chapter 7

Proof-producing contextual recursion

We propose a generic algorithm for term transformations, based on structural recursion. The algorithm is parameterized by a few simple plugin functions embodying the essence of the transformation. By combining compatible plugin functions, we can perform several transformations in one traversal. Transformations can depend on some context that encapsulates relevant information, such as bound variables, variable substitutions, and polarity. Each transformation can define its own notion of context that is threaded through the recursion.

The output is generated by a proof module that maintains a stack of derivation trees. The procedure apply(R, n, Γ, t, u) pops n derivation trees Dn from the stack and pushes the tree

onto the stack.The plugin functions are responsible for invoking apply as appropriate.

The generic algorithm and its instantiations

The algorithm performs a depth-first postorder contextual recursion on the term to process.

Subterms are processed first; then an intermediate term is built from the resulting subterms and is processed itself. The context ∆ is updated in a transformation-specific way with each recursive call. It is abstract from the point of view of the algorithm.

The plugin functions are divided into two groups: ctx-let, ctx-quant, and ctx-app update the context when entering the body of a binder or when moving from a function symbol to one of its arguments; build-let, build-quant, build-app, and build-var return the processed term and produce the corresponding proof as a side effect.

function process(∆, t) match t case x: return build-var(∆, x) case f( tn ):

'Let' expansion

The first instance of the contextual recursion algorithm expands 'let' expressions and renames bound variables systematically to avoid capture. Skolemization and theory simplification, presented below, assume that this transformation has been performed.

The context consists of a list of fixed variables and variable substitutions, as in Sect. 6.1.

The plugin functions are as follows:

The ctx-let and build-let functions process 'let' expressions. In ctx-let, the substituted terms are processed further before they are added to a substitution entry in the context. In build-let, the Let rule is applied and the transformed term is returned. Analogously, the ctx-quant and build-quant functions rename quantified variables systematically. This ensures that any variables that arise in the range of the substitution specified by ctx-let will resist capture when the substitution is applied (cf. Example 6.4). Finally, the ctx-app, build-app, and build-var functions simply reproduce the term traversal in the generated proof; they perform no transformation-specific work.

Skolemization

Our second transformation, skolemization, assumes that 'let' expressions have been expanded

and bound variables have been renamed apart. The context is a pair ∆ = (Γ, p), where Γ is a context as defined in Sect. 6.1 and p is the polarity (+, -, or ?) of the term being processed.

The main plugin functions are those that manipulate quantifiers:

The polarity component of the context is updated by ctx-app, which is not shown. For example, ctx-app((Γ, -), ¬, ϕ, 1) returns (Γ, +), because if ¬ ϕ occurs negatively in a larger formula, then ϕ occurs positively. The plugin functions build-app and build-var are as for 'let' expansion.

Positive occurrences of ∃ and negative occurrences of ∀ are skolemized. All other quantifiers are kept as is. The sko_term function returns an applied Skolem function symbol following some reasonable scheme; for example, outer skolemization [START_REF] Nonnengart | Computing Small Clause Normal Forms[END_REF] creates an application of a fresh function symbol to all variables fixed in the context. To comply with the inference system, the application of Sko ∃ or Sko ∀ in build-quant instructs the proof module to systematically replace the Skolem term with the corresponding ε term when outputting the proof. The resulting derivation tree is as in Example 6.2.

Theory simplification

All kinds of theory simplification can be performed on formulas. We restrict our focus to a simple yet quite characteristic instance: the simplification of u + 0 and 0 + u to u. We assume that 'let' expressions have been expanded. The context is a list of fixed variables. The plugin functions ctx-app and build-var are as for 'let' expansion (Sect. 7.1.1); the remaining ones are presented below:

The quantifier manipulation code, in ctx-quant and build-quant, is straightforward. The interesting function is build-app. It first applies the Cong rule to justify rewriting the arguments.

Then, if the resulting term f(ū n ) can be simplified further into a term u, it performs a transitive chain of reasoning:

Assuming that the framework has been instantiated with theory simplification for additive and multiplicative identity, invoking process(∅, ϕ) returns the formula k < k. The generated derivation tree is as in Example 6.3.

Combinations of transformations

Theory simplification can be implemented as a family of transformations, each member of which embodies its own set of theory-specific rewrite rules. If the union of the rewrite rule sets is confluent and terminating, a unifying implementation of build-app can apply the rules in any order until a fixpoint is reached. Moreover, since theory simplification modifies terms independently of the context, it is compatible with 'let' expansion and skolemization. This means that we can replace the build-app implementation from Sect. 7.1.1 or 7.1.2 with that of Sect. 7.1.3. In particular, this allows us to perform arithmetic simplification in the substituted terms of a 'let' expression in a single pass (cf. Example 6.1).

The combination of 'let' expansion and skolemization is less straightforward. Consider the formula ϕ = let y ∃x. p(x) in y → y. When processing the subformula ∃x. p(x), we cannot (or at least should not) skolemize the quantifier, because it has no unambiguous polarity; indeed, the variable y occurs both positively and negatively in the 'let' expression's body. We can of course give up and perform two passes: The first pass expands 'let' expressions, and the second pass skolemizes and simplifies terms. The first pass also provides an opportunity to expand equivalences, which are problematic for skolemization.

There is also a way to perform all the transformations in a single instance of the framework.

The most interesting plugin functions are ctx-let and build-var:

function build-var((Γ, p), x) apply(Refl, 0, Γ, x, Γ(x)) u ← process((Γ, p), Γ(x)) apply(Trans, 2, Γ, Γ(x), u) return u

In contrast with the corresponding function for 'let' expansion (Sect. 7.1.1), ctx-let does not process the terms rn , which is reflected by the n applications of Refl, and it must thread through polarities. The call to process is in build-var instead, where it can exploit the more precise polarity information to skolemize the formula.

The build-let function is essentially as before. The ctx-quant and build-quant functions are as for skolemization (Sect. 7.1.2), except that the else cases rename bound variables apart (Sect. 7.1.1). The ctx-app function is as for skolemization, whereas build-app is as for theory simplification (Sect. 7.1.3).

For the formula ϕ given above, process((∅, +), ϕ) returns (∃x. p(x)) → p(c), where c is a fresh Skolem constant. The substituted term ∃x. p(x) is put unchanged into the substitution used to expand the 'let' expression. It is processed each time y arises in the body y -→ y.

The positive occurrence is skolemized; the negative occurrence is left as is. Using caching and a DAG representation of derivations, we can easily avoid the duplicated work that would arise if y occurred several times with positive polarity.

Scope and limitations

Other possible instances of contextual recursion are the clause normal form (CNF) transformation and the elimination of quantifiers using one-point rules. CNF transformation is an instance of rewriting of Boolean formulas and can be justified by a Taut Bool rule. Tseytin transformation can be supported by representing the introduced constants by the formulas they represent, similarly to our treatment of Skolem terms. One-point rules-e.g., the transformation of ∀x. x a -→ p(x) into p(a)-are similar to 'let' expansion and can be represented in much the same way in our framework. The rules for eliminating universal and existential quantifiers are as follows:

The plugin functions used by process would also be similar as those for 'let' expansion, except that detecting the assignment at ctx-quant requires examining the body of the quantified formula to determine whether the one-point rule is applicable. Some transformations, such as symmetry breaking [START_REF] Déharbe | Exploiting Symmetry in SMT Problems[END_REF] and rewriting based on global assumptions, require a global analysis of the problem that cannot be captured by local substitution of equals for equals. They are beyond the scope of the framework. Other transformations, such as simplification based on associativity and commutativity of function symbols, require traversing the terms to be simplified when applying the rewriting. Since process visits terms in postorder, the complexity of the simplifications would be quadratic, while a processing that applies depth-first preorder traversal can perform the simplifications with a linear complexity.

Hence, applying such transformations optimally is also outside the scope of the framework.

Correctness

We turn to the contextual recursion algorithm that generates derivations in that system. The first question is, Are the derivation trees valid? In particular, it is not obvious from the code that the side conditions of the inference rules are always satisfied. First, we need to introduce some terminology. A term is shadowing-free if nested binders always bind variables with different names; for example, the term ∀x. (∀y. p(x, y)) ∧ (∀y. q(y)) is shadowing-free, while ∀x. (∀x. p(x, y)) ∧ (∀y. q(y)) is not. The set of variables fixed by Γ is written fix (Γ), and the set of variables replaced by Γ is written repl (Γ). They are defined as follows:

Trivial substitutions x → x are ignored, since they have no effect. The set of variables introduced by Γ is defined by intr (Γ) = fix (Γ) ∪ repl (Γ). A context Γ is consistent if all the fixed variables are mutually distinct and the two sets of variables are disjoint-i.e., fix (Γ) ∩ repl (Γ) = {}.

A judgment Γ t u is canonical if Γ is consistent, FV(t) ⊆ intr (Γ), FV(u) ⊆ fix (Γ), and BV(u) ∩ intr (Γ) = {}. The canonical inference system is a variant of the system of Sect. 6.1 in which all judgments are canonical and rules Trans, Bind, and Let have no side conditions.

Lemma 7.1. Any inference in the canonical inference system is also an inference in the original inference system.

Proof. It suffices to show that the side conditions of the original rules are satisfied.

Case Trans: Since the first judgment in the antecedent is canonical, FV(t) ⊆ fix (Γ). By consistency of Γ, we have fix (Γ) ∩ repl (Γ) = {}. Hence, FV(t) ∩ repl (Γ) = {} and therefore

Case Bind: Since the succedent is canonical, we have that (1) FV(Qx. ϕ) ⊆ intr (Γ) and

(2) BV(Qy. ψ) ∩ intr (Γ) = {} hold. From (2), we deduce y / ∈ intr (Γ). Hence, by (1), we get y / ∈ FV(Qx. ϕ).

Case Let: Similar to Trans.

Theorem 7.2 (Total Correctness of Recursion). For the instances presented in Sects. 7.1.1 to 7.1.3, the contextual recursion algorithm always produces correct proofs.

Correctness

Proof. The algorithm terminates because process is called initially on a finite input and recursive calls always have smaller inputs.

For the proof of partial correctness, only the Γ part of the context is relevant. We will write process(Γ, t) even if the first argument actually has the form (Γ, p) for skolemization. The pre-and postconditions of a process(Γ, t) call that returns the term u are Pre1 Γ is consistent;

Post1 u is shadowing-free;

For skolemization and simplification, we may additionally assume that bound variables have been renamed apart by 'let' expansion, and hence that the term t is shadowing-free.

The initial call process(∅, t) trivially satisfies the preconditions on an input term t that contains no free variable. We must show that the preconditions for each recursive call process(Γ , t ) are satisfied and that the postconditions hold at the end of process(Γ, t).

Pre1 (Γ is consistent): First, we show that the fixed variables are mutually distinct. For 'let' expansion, all fixed variables are fresh. For skolemization and simplification, a precondition is that the input is shadowing-free. For any two fixed variables in Γ , the input formula must contain two quantifiers, one in the scope of the other. Hence, the variables must be distinct.

Second, we show that fix (Γ ) ∩ repl (Γ ) = {}. For 'let' expansion, all fixed variables are fresh.

For skolemization, the condition is a direct consequence of the precondition that the input is shadowing-free. For simplification, we have repl (Γ ) = {}.

Pre2 (FV(t ) ⊆ intr (Γ )): We have FV(t) ⊆ intr (Γ). The desired property holds because the ctx-let and ctx-quant functions add to the context any bound variables that become free when entering the body t of a binder.

Pre3 (BV(t ) ∩ fix (Γ ) = {}): The only function that fixes variable is ctx-quant. For 'let' expansion, all fixed variables are fresh. For skolemization and simplification, the condition is a consequence of the shadowing-freedom of the input.

Post1 (u is shadowing-free): The only function that builds quantifiers is build-quant. The process(Γ , ϕ) call that returns the processed body ψ of the quantifier is such that y ∈ intr (Γ )

in the 'let' expansion case and x ∈ intr (Γ ) in the other two cases. The induction hypothesis ensures that ψ is shadowing-free and BV(ψ) ∩ intr (Γ ) = {}; hence, the result of build-quant (i.e., Qy.ψ or Qx.ψ) is shadowing-free. Quantifiers can also emerge when applying a substitution in build-var. This can happen only if ctx-let has added a substitution entry to the context, in which case the substituted term is the result of a call to process and is thus shadowing-free.

Post2 (FV(u) ⊆ fix (Γ)): In most cases, this condition follows directly from the induction hypothesis Post2. The only case where a variable appears fixed in the context Γ of a recursive call to process and not in Γ is when processing a quantifier, and then that variable is bound in the result. For variable substitution, it suffices to realize that the context in which the substituted term is created (and which fixes all the free variables of the term) is a prefix of the context when the substitution occurs.

Post3 (BV(u) ∩ intr (Γ) = {}): In most cases, this condition follows directly from the induction hypothesis Post3: For every recursive call, intr (Γ) ⊆ intr (Γ ). Two cases require attention. For 'let' expansion, a variable may be replaced by a term with bound variables. Then the substituted term only contains variables that do not occur in the input. The variables introduced by Γ will be other fresh variables or variables from the input. The second case is when a quantified formula is built. For 'let' expansion, a fresh variable is used. For skolemization and simplification, we have BV(Qx. ϕ) ∩ fix (Γ) = {} (Pre3); hence x / ∈ fix (Γ). Finally, we must show that x / ∈ repl (Γ);

this is a consequence of the shadowing-freedom of the input.

It is easy to see that each apply call generates a rule with an antecedent and a succedent of the right form, ignoring the rules' side conditions. Moreover, all calls to apply generate canonical judgments thanks to the pre-and postconditions proved above. Correctness follows from Lemma 7.1.

Observation 7.3 (Complexity of Recursion). For the instances presented in Sects. 7.1.1 to 7.1.3, the 'process' function is called at most once on every subterm of the input.

Justification. It suffices to notice that a call to process(∆, t) induces at most one call for each of the subterms in t.

As a corollary, if all the operations performed in process excluding the recursive calls can be accomplished in constant time, the algorithm has linear-time complexity with respect to the input. There exist data structures for which the following operations take constant time:

extending the context with a fixed variable or a substitution, accessing direct subterms of a term, building a term from its direct subterms, choosing a fresh variable, applying a context to a variable, checking if a term matches a simple template, and associating the parameters of the template with the subterms. Thus, it is possible to have a linear-time algorithm for 'let' expansion and simplification.

On the other hand, construction of Skolem terms is at best linear in the size of the context and of the input formula in process. Hence, skolemization is at best quadratic in the worst case. This is hardly surprising because in general, the formula ∀x 1 . ∃y 1 . . . . ∀x n . ∃y n . ϕ[x n , ȳn ], whose size is proportional to n, is translated to ∀x

whose size is quadratic in n.

Observation 7.4 (Overhead of Proof Generation). For the instances presented in Sects. 7.1.1 to 7.1.3 , the number of calls to the 'apply' procedure is proportional to the number of subterms in the input.

Justification. This is a corollary of Observation 7.3, since the number of apply calls per process formed in preprocessing steps were represented in the proof in a very coarse manner, amounting to gaps in the proof. For example, when 'let' expressions were expanded in a formula, the only information present in the proof would be the formula before and after 'let' expansion.

When extending veriT to generate more detailed proofs, we were able to reuse its existing proof module and proof format [START_REF] Besson | A Flexible Proof Format for SMT: a Proposal[END_REF]. A proof is a list of inferences, each of which consists of an identifier (e.g., .c0), the name of the rule, the identifiers of the dependencies, and the derived clause. The use of identifiers makes it possible to represent proofs as DAGs. We extended the format with the inference rules of Sect. 6.1. The rules that augment the context take a sequence of inferences-a subproof -as a justification. The subproof occurs within the scope of the extended context. Following this scheme, the skolemization proof for the formula ¬ ∀x.

Formerly, no details of these transformations would be recorded. The proof would have contained only the original formula and the skolemized result, regardless of how many quantifiers appeared in the formula.

In contrast with the abstract proof module described in Sect. 7.1, veriT leaves Refl steps implicit for judgments of the form Γ t t. The other inference rules are generalized to cope with missing Refl judgments. In addition, when printing proofs, the proof module can automatically replace terms in the inferences with some other terms. This is necessary for transformations such as skolemization and 'if-then-else' elimination. We must apply a substitution in the replaced term if the original term contains variables. In veriT, efficient data structures are available to perform this.

Transformations

The implementation of contextual recursion uses a single global context, augmented before processing a subterm and restored afterwards. The context consists of a set of fixed variables, a substitution, and a polarity. In our setting, the substitution satisfies the side conditions by construction. If the context is empty, the result of processing a subterm is cached. For skolemization, a separate cache is used for each polarity. No caching is attempted under binders.

Invoking process on a term returns the identifier of the inference at the root of its transformation proof in addition to the processed term. These identifiers are threaded through the recursion to connect the proof. The proofs produced by instances of contextual recursion are inserted into the larger resolution proof produced by veriT. This is achieved through an inference of the form

where ϕ is the original formula, ψ is the processed formula, and D is a derivation of ϕ ψ.

The derivation D may itself depend on instances of rule Taut T , each with its own proof of the side condition that must also be included in the overall proof.

Transformations performing theory simplification were straightforward to port to the new framework: Their build-app functions simply apply rewrite rules until a fixpoint is reached. Porting transformations that interact with binders required special attention in handling the context and producing proofs. Fortunately, most of these aspects are captured by the inference system and the abstract contextual recursion framework, where they can be studied independently of the implementation.

Some transformations are performed outside of the framework. Proofs of CNF transformation are expressed using the inference rules of veriT's underlying SAT solver, so that any tool that can reconstruct SAT proofs can also reconstruct these proofs. Simplification based on associativity and commutativity of function symbols is implemented as a dedicated procedure, for efficiency reasons (Sect. 7.1.5). It currently produces coarse-grained proofs.

Evaluation

To evaluate the impact of the new contextual recursion algorithm and of producing detailed proofs, we compare the performance of different configurations of veriT. Our experimental data is available online. 1 We distinguish three configurations. Basic only applies transformations for which the old code provided some (coarse-grained) proofs. Extended also applies transformations for which the old code did not provide any proofs, whereas the new code provides detailed proofs. Complete applies all transformations available, regardless of whether they produce proofs.

More specifically, Basic applies the transformations for 'let' expansion, skolemization, elimination of quantifiers based on one-point rules, elimination of 'if-then-else', theory simplification for rewriting n-ary symbols as binary, and elimination of equivalences and exclusive disjunctions with quantifiers in subterms. Extended adds Boolean and arithmetic simplifications to the transformations performed by Basic. Complete performs global rewriting simplifications and symmetry breaking in addition to the transformations in Extended.

The evaluation was carried out on two main sets of benchmarks from SMT-LIB [START_REF] Barrett | The SMT-LIB Standard: Version 2.5[END_REF] 2 : the 20 916 benchmarks, labeled as satisfiable or unsatisfiable, in the quantifier-free (QF) categories QF_ALIA, QF_AUFLIA, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFIDL, QF_UFLIA, and QF_UFLRA; and the 30 250 benchmarks labeled as unsatisfiable in the non-QF categories AUFLIA, AUFLIRA, UF, UFIDL, UFLIA, and UFLRA. The categories with 1 http://matryoshka.gforge.inria.fr/pubs/processing/ 2 As of February 2017.