Bases de données, contraintes d'intégrité et logiques modales
Institution:
Paris 11Disciplines:
Directors:
Abstract EN:
In this thesis, we use tableaux system for modal logics in order to solve databases problems related to integrity constraints. In first part, we use a tableaux system for first order modal logics in the context of a method testing integrity constraints preservation in an object oriented database. We develop a proof search strategy and we prove that it is sound and complete in its unbounded version. This leads to the implementation of a theorem prover for first order modal logics k, k4, d, t and s4. The prover can also be used for other applications where the test of validity of first order modal logics is needed (software verification, multi-agents systems, etc. ). In second part, we study hybrid multi-modal logic (hmml) as a formalism to express schemas and integrity constraints for semi-structured data. On the one hand we prove that hmml captures the notion of semi-structured data and constraints on it. On the other hand we generalize the notion of schema, by proposing a definition of schema where references are "well typed" (contrary to what happens with dtds), and we prove that this new notion can be formalized by sentences of hmml exactly like a constraint is. When a tableaux system for the hmml is added to this approach, some classical database problems can be treated (constraints implication, schemas inclusion, constraints satisfiability, etc. ).
Abstract FR:
Dans cette these, nous nous etudions l'utilisation des systemes par tableaux pour les logiques modales dans le cadre de problemes lies aux contraintes d'integrite dans lesbases de donnees. Dans une premiere partie, nous utilisons un systeme par tableaux, traitant differentes logiques modales du premier ordre (lmpo), dans le cadre d'une methode permettant de tester la preservation de contraintes d'integrite dynamiques dans des bases de donnees orientees objet. Nous associons a ce systeme une strategie de recherche de preuve que nous prouvons correcte et complete dans sa version non bornee, ceci nous permet d'implanter un demonstrateur automatique detheoremes pour les lmpo k, k4, d, t et s4. Ce demonstrateur est re-utilisable pour d'autres applications necessitant de prouver la validite de formules des lmpo (verification de logiciel,systeme multi-agents, etc. ). Dans une seconde partie, nous etudions l'utilisation de la logique multi-modale hybride (lmmh) en tant que formalisme d'expression de schema et de contraintes pour les donnees semi-structurees. D'une part, nous prouvons que la lmmh permet de capturer directement la notion de donnees semi-structurees et donc de contraintes sur ces donnees. D'autre part, nous proposons une extention des dtd permettant le typage des references et nous montrons que cette nouvelle notion de schemapeut etre formalisee en termes de formules de la lmmh exactement comme une contrainte. En associant un systeme par tableaux pour la lmmh a cette approche, il est alors possible de traiter beaucoup de problemes classiques de bases de donnees (implication de contraintes, inclusion de schemas, satisfaisabilite de contraintes, etc. ).