Vérification D'une Méthode De Preuve Pour La Logique De Description Alc
Résumé: Les logiques de description (DLs) sont une famille de langages utilisés pour la représentation et le raisonnement sur des connaissances d’un domaine d’application d’une manière structurée et formelle. Pour atteindre cet objectif, plusieurs raisonneurs ont été implantés, comme RACER et FACT++. Toutes ces implantations n’ont pas encore été certifiées. Pour garantir la correction des déri- vations des propriétés dans les DLs, il s’avère nécessaire de valider formellement le processus de raisonnement appliqué aux DLs. Dans ce papier, nous présentons une définition d’un raisonneur pour la logique de description ALC basé sur la méthode du tableau sémantique. On assure la validité de notre raisonneur par la preuve des propriétés de son adéquation, de sa complétude et de sa terminaison dans l’assistant de preuve Isabelle/HOL. La preuve procède en deux étapes: elle établit les propriétés sur un niveau abstrait, ensembliste, et les instancie ensuite pour une implantation sur des listes.
Mots-clès:
Nos services universitaires et académiques
Thèses-Algérie vous propose ses divers services d’édition: mise en page, révision, correction, traduction, analyse du plagiat, ainsi que la réalisation des supports graphiques et de présentation (Slideshows).
Obtenez dès à présent et en toute facilité votre devis gratuit et une estimation de la durée de réalisation et bénéficiez d'une qualité de travail irréprochable et d'un temps de livraison imbattable!
Aucun fichier associé
Si le fichier est volumineux, l'affichage peut échouer. Vous pouvez obtenir le fichier directement en cliquant sur le bouton "Télécharger".
