up: Publications

Formalisation de la logique de description ALC dans l'assistant de preuve Coq

Mohamed Chaabani, Mohamed Mezghiche, Martin Strecker



 
 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