up: Publications |
Abstract |
Le langage d'ontologie Web (Web Ontology Language OWL) est un langage
utilisé pour le web sémantique. OWL est basé sur les logiques de
description (LD), une famille de langages adaptés pour la
représentation et le raisonnement sur des connaissances d'un domaine
d'application d'une façon structurée et formelle. Le web sémantique
est actuellement l'un des champs d'application des méthodes formelles,
dont l'objectif est d'assurer leur fiabilité. Un point essentiel de
l'application de ces méthodes formelles est la preuve de validité des
raisonnements dans des LDs, comme celle de la terminaison,
l'adéquation (soundness) et la complétude d'un raisonneur. Dans ce
papier, on présente une spécification formelle de la syntaxe et de la
sémantique de ALC, qui est considérée comme un
représentant typique d'une large gamme de LDs. On prouve pour cette
logique les propriétés d'adéquation, de complétude et de terminaison
dans l'assistant de preuve Coq.
Online Copy |
Available as conference version and long version
BibTeX Entry |
@InProceedings{chaabani09:_formal_de_la_logiq_descr, author = {Mohamed Chaabani and Mohamed Mezghiche and Martin Strecker}, title = {Formalisation de la logique de description ALC dans l'assistant de preuve Coq}, booktitle = {Proc. 3es Journ{\'e}es francophones sur les ontologies}, pages = {139-147}, year = 2009, month = dec }
Last modified: Thu Oct 8 14:50:30 CEST 2009 |