Dialog Between Logic, Trees and Circuits - CRISTAL-SPIRALS
Hdr Année : 2024

Dialog Between Logic, Trees and Circuits

Dialogue entre Logique, Arbres et Circuits

Résumé

Since my post-doctorate, I have mainly worked on the foundation of data and knowledge management. In my habilitation, I focus on some of my main contributions over the following questions: reasoning of logical formula over relational instance, reasoning and evaluating queries over trees, and reasoning over circuits. My contributions are organised into three parts: a dialogue between logical reasoning and reasoning over trees; a dialogue between tree evaluation and querying circuit and finally a dialogue between the explanation of query evaluation and circuits. The first part focuses on translating logical problems into reasoning problems over trees and vice versa. First, I present different reductions of reasoning on fixpoint logic into reasoning on tree automata in order to obtain some efficient upper bound over the logical reasoning. Secondly, I explain how the validity problem of a tree automata into a union of conjunctive queries can be used to prove different lower bounds on logical reasoning.

In the second part, I present an approach proposed by my co-authors and me to reduce different problems of enumeration of solutions of tree automata evaluation over trees into the same enumeration problems over a particular kind of circuit allowing to solve this problem efficiently. Finally, I present different results on the computation of provenance for Datalog, a well-known recursive language for querying databases. First, I present an approach based on techniques presented in previous parts giving an FPT algorithm to efficiently compute the Boolean provenance for a subclass of Datalog programs. Then, I present a discussion about different semantics to compute the provenance for Datalog comparing them together and following some desired properties.

Mon habilitation porte principalement sur les résultats fondamentaux que j'ai développé depuis mon post-doctorat. Ceux-ci se sont focalisés sur la relation entre différents questions: les raisonnements sur les formules logiques dans le cadre relationnel, le raisonnement et l'évaluation de requêtes sur les arbres et l'évaluation sur les circuit logiques. Dans le cadre de mes travaux sur la gestion des connaissances, j'ai étudié le raisonnement sur de formules de logiques avec point fixes. J'ai travaillé sur la réduction des problèmes de raisonnements sur des instances relationnelles vers des problèmes de raisonnements sur les arbres et vice versa. Ces travaux ont porté sur la traduction de formule logique en automate d'arbres permettant d'obtenir des bornes supérieures sur les raisonnements de formules et sur la traduction du problème de validité d'un automate d'arbre au regard d'une requête conjonctive dans un problème de raisonnement sur la logique étudiée permettant d'obtenir des bornes inférieures sur ce dernier problème. En particulier, nous étudions une logique de point fixe appelée GNFP-UP et montrant les bornes inférieures pour l'inclusion de programmes Monadic Datalog qui était une question ouverte dans la communauté. Le deuxième grand axe de recherche sur lequel j'ai travaillé est la relation entre les circuits logiques et l'évaluation de requêtes sur les arbres et les mots. Nous montrons que la trace de l'évaluation d'une requête MSO sur un arbre, appelée provenance peut être décrite au travers un circuit booléen possédant une structure particulière appelée d-DNNF de même que les réponses de cette requête. Au travers l'étude de ce type de circuit, nous avons pu redémontrer que l'énumération des réponses peut se faire avec un précalcul linéaire et un délai constant et que nous pouvions mettre à jour efficacement le circuit sous-jacent. Nous avons étendu notre approche pour énumérer les réponses suivant un ordre donné par une fonction d'agrégation sur les valeurs des réponses. Pour finir, j'ai travaillé sur la notion de provenance et sa représentation en circuit. La notion de provenance en base de données est une méthode permettant de représenter et calculer différentes informations autour de l'évaluation des données. Une représentation par circuits permet de représenter efficacement tout un ensemble de provenances. Plusieurs questions se posent dans ce cadre, comment bien définir la notion de provenance, comment l'évaluer efficacement et dans quel contexte. Tout d'abord, nous avons proposé une approche FPT pour calculer la provenance booléenne pour un sous langage de Datalog sur une instance ICG en utilisant des techniques développées dans les autres parties. Nous investiguons aussi différentes sémantiques pour la provenance afin de comprendre les limitations. La définition classique de la provenance pour Datalog impose de raisonner sur un nombre infini de structures limitant son usage. Nous comparons ces différentes sémantiques entre elles mais aussi au regard de propriétés désirées.
Fichier principal
Vignette du fichier
hdr.pdf (1.08 Mo) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

tel-04743648 , version 1 (18-10-2024)

Identifiants

  • HAL Id : tel-04743648 , version 1

Citer

Pierre Bourhis. Dialog Between Logic, Trees and Circuits. Computer Science [cs]. Université de Lille, 2024. ⟨tel-04743648⟩
0 Consultations
0 Téléchargements

Partager

More