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 :
|
Tous les documents dans DSpace sont protégés par copyright, avec tous droits réservés.
|