Date : 1993
Editeur / Publisher : Marseille : [s.n.] , 1993
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : français / French
Résumé / Abstract : Pour raisonner automatiquement sur des bases de connaissances incomplètes, nous utilisons un formalisme non monotone particulier: la théorie des hypothèses. Définie comme une logique multimodale, elle possède un langage précis, une sémantique bien définie et surtout une propriété de compacité garantissant l'existence d'une procédure de preuve, ce qui autorise la définition d'un mécanisme de raisonnement automatique. Comme pour les logiques des défauts de Reiter, cette théorie permet la génération d'ensembles de croyances ou extensions de la théorie initiale. Nous montrons que la question de l'appartenance d'une formule à une extension peut se ramener à un problème de production (consequence finding): une formule appartient à une extension si en ajoutant sa négation à la théorie, on peut dériver une disjonction de négations d'hypothèses. Cette thèse présente une méthode de production basée sur la saturation par résolution de l'ensemble de départ. Pour établir cette méthode, nous définissons une méthode de résolution adéquate et complète basée sur des formules en forme clausale multimodale. Cette forme clausale est obtenue par transformation des formules multimodales en pseudo-clauses formules dans lesquelles les opérateurs modaux ne contiennent que des disjonctions. L'originalité et l'intérêt de cette transformation est qu'elle permet d'obtenir à partir d'une formule f un ensemble de clauses dont la longueur dépend linéairement de f, et qu'elle est utilisable pour toute logique multimodale. Elle offre ainsi de nouvelles perspectives dans l'utilisation du principe de résolution en logique modale.