DSpace À propos de l'application DSpace
 

Depot Institutionnel de l'UMBB >
Publications Scientifiques >
Communications Internationales >

Veuillez utiliser cette adresse pour citer ce document : http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/11211

Titre: Formalisation de la logique de description ALC dans l'assistant de preuve Coq
Auteur(s): Chaabani, Mohamed
Mezghiche, Mohamed
Strecker, Martin
Mots-clés: Logiques de Description
Methodes formelles
OWL-DL
Tableau semantique
Adequation
Date de publication: 2009
Collection/Numéro: Proc. 3es Journ{\'e}es francophones sur les ontologies;pp. 139-147
Résumé: Le langage d’ontologie Web (Web Ontology Language OWL) est un langage utilis ́e pour le web s ́emantique. OWL est bas ́e sur les logiques de description (LD), une famille de lan- gages adapt ́es pour la repr ́esentation et le raisonnement sur des connaissances d’un domaine d’application d’une fa ̧con structur ́ee et formelle. Le web s ́emantique est actuellement l’un des champs d’application des m ́ethodes formelles, dont l’objectif est d’assurer leur fiabilit ́e. Un point essentiel de l’application de ces m ́ethodes formelles est la preuve de va- lidit ́e des raisonnements dans des LDs, comme celle de la terminaison, l’ad ́equation (soundness) et la compl ́etude d’un raisonneur. Dans ce papier, on pr ́esente une sp ́ecification formelle de la syntaxe et de la s ́emantique de ALC, qui est consid ́er ́ee comme un repr ́esentant typique d’une large gamme de LDs. On prouve pour cette logique les pro- pri ́et ́es d’ad ́equation, de compl ́etude et de terminaison dans l’assistant de preuve Coq.
URI/URL: http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/11211
Collection(s) :Communications Internationales

Fichier(s) constituant ce document :

Fichier Description TailleFormat
CHABANI1.pdf215,93 kBAdobe PDFVoir/Ouvrir
View Statistics

Tous les documents dans DSpace sont protégés par copyright, avec tous droits réservés.

 

Valid XHTML 1.0! Ce site utilise l'application DSpace, Version 1.4.1 - Commentaires