La génération de conséquences en logique modale
Institution:
Toulouse 3Disciplines:
Directors:
Abstract EN:
The key notion in consequence finding is that of prime implicates, which are defined to be the logically strongest clausal consequences of a formula. Prime implicates have proven useful in artificial intelligence, especially in knowledge compilation and abductive reasoning. In this thesis, we extend the investigation of prime implicates from propositional logic to the basic multi-modal logic Kn. We begin by comparing the properties of several plausible definitions of prime implicates in Kn in order to isolate the most suitable definition. We next study the computational aspects of the selected definition. Specifically, we provide algorithms for prime implicate generation and recognition, and we study the complexity of these tasks. Finally, we show how our notion of prime implicates can be used to define a normal form for Kn with interesting knowledge compilation properties.
Abstract FR:
La notion clé de la génération de conséquences est celle de l'impliqué premier, qui désigne une clause qui est impliquée par une formule et telle qu'il n'existe pas de clause logiquement plus forte impliquée par la formule. La notion d'impliqué premier s'est montrée très utile en intelligence artificielle, notamment pour la compilation de connaissances et le raisonnement abductif. Dans cette thèse nous étudions comment cette notion, jusqu'à présent étudiée en logique propositionnelle, peut être étendue à la logique modale Kn. Nous commençons par comparer plusieurs definitions plausibles d'impliqués premiers dans Kn, avant d'en selectionner une. Ensuite, nous proposons des algorithmes pour générer et reconnaître des impliqués premiers, et nous étudions la complexité de ces deux tâches. Puis, nous utilisons notre notion d'impliqué premier pour élaborer une forme normale pour Kn qui est dotée de propriétés intéressantes du point de vue de la compilation de connaissances.