Techniques de déduction automatique vues comme recherche de preuve en calcul des séquents

139 pagesComputer-aided reasoning plays a great role in computer science and mathematical logic, from logic programing to automated reasoning, via interactive proof assistants, etc. The general aim of this thesis is to design a general framework where various techniques of Computer-aided reasoning can be implemented, so that they can collaborate, be generalised, and implemented in a safe and trusted way. The framework I propose is a sequent calculus called LKp(T), which generalises an older calculus of the literature to the presence of an arbitrary background theory for which we have a decision procedure, like linear arithmetic. The thesis develops the meta-theory of LKp(T), such as its logical completeness. We then show how it specifies a proof-search procedure that can emulate a well-known technique from the field of Satisfiability-modulo-Theories, namely DPLL(T). Finally, clause and connection tableaux are other widely used techniques of automated reasoning, of a rather different nature from that of DPLL. This thesis also described how such tableaux techniques can be described as bottom-up proof-search in LKp(T). The simulation is given for both propositional and first-order logic, opening up new perspectives of generalisation and collaboration between tableaux techniques and DPLL, even in presence of a background theory.Le raisonnement assisté par ordinateur joue un rôle crucial en informatique et en logique mathématique, de la programmation logique à la déduction automatique, en passant par les assistants à la démonstration. Le but de cette thèse est la conception d'un cadre général où différentes techniques de raisonnement assisté par ordinateur peuvent être implémentées, pour que ces dernières puissent collaborer, être généralisées, et être implémentées de manière plus sûre. Le cadre que je propose est un calcul des séquents appelé LKp(T), qui généralise un système de la littérature à la présence d'une théorie pour laquelle nous avons une procédure de décision, comme l'arithmétique linéaire. Cette thèse développe la méta-théorie de LKp(T), avec par exemple la propriété de complétude logique. Nous montrons ensuite comment le système spécifie une procédure de recherche de preuve qui émule une technique connue du domaine de la Satisfiabilité-modulo-théories appelée DPLL(T). Enfin, les tableaux de clauses et les tableaux de connexions sont d'autres techniques populaires en déduction automatique, d'une nature relativement différente de DPLL. Cette thèse décrit donc également comment ces techniques de tableaux peuvent être décrites en termes de recherche de preuve dans LKp(T). La simulation est donnée à la fois pour la logique propositionnelle et la logique du premier ordre, ce qui ouvre de nouvelles perspectives de généralisation et de collaboration entre les techniques de tableaux et DPLL, même en présence d'une théorie