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.
| Identifer | oai:union.ndltd.org:CCSD/oai:pastel.archives-ouvertes.fr:pastel-00961344 |
| Date | 19 December 2013 |
| Creators | Farooque, Mahfuza |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0018 seconds