Date : 2005
Editeur / Publisher : [S.l.] : [s.n.] , 2005
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : français / French
Résumé / Abstract : De nombreux travaux ont montré l'importance de l'interpolation de Craig pour la structuration et la modularité des spécifications de type axiomatique. En vue d'en donner des conditions suffisantes dans un cadre théorique adapté à l'informatique, nous nous sommes intéressé à une propriété équivalente à l'interpolation de Craig dans le cadre de la théorie standard des modèles : la consistance de Robinson. L'étude de cette dernière propriété nous a amené à généraliser dans une spécialisation des institutions les notions classiques de diagrammes complets et de morphismes élémentaires. Ceci nous a alors permis de généraliser quelques résultats classiques de théorie des modèles tels que les théorèmes de Löwenheim-Skolem ou l'union de chaînes de Tarski. En fin, les constructeurs de formules étant explicites dans notre cadre théorique, nous nous sommes naturellemant intéressés à la combinaison de logiques et à la préservation de l'interpolation de Craig et de la consistance de Robinson.
Résumé / Abstract : The importance of Craig interpolation for structuration and modularity of axiomatic style specifications have been shown by many works. In order to give sufficient conditions to Craig interpolation in a suitable framework for computer science, we've studied a propery equivalent to Craig interpolation in standard model theory: Robinson consistency. To do so, we had to generalize the notions of complete diagrams and elementary morphisms in a specialization of institutions. This allowed the generalization of other classical standard model theory results such as Löwenheim-Skolem theorem and Tarski chain union. Finally, since formulae constructors are explicite in our framework, we've studied logic combination and the preservation of both Craig interpolation and Robinson consistency through combination.