Vérification d'une méthode de preuve pour la logique de description ALC

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érivations 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 $\mathcal{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.
 

Online Copy

Available as PDF

BibTeX Entry

@InProceedings{chaabani10:_verif_alc,
  author = 	 {Mohamed Chaabani and Mohamed Mezghiche and Martin Strecker},
  title = 	 {V{\'e}rification d'une m{\'e}thode de preuve pour la logique de
  description {$\cal{ALC}$}},
  booktitle =    {Proc. 10{\`e}me Journ{\'e}es Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels (AFADL)},
  editor = {Ait-Ameur, Yamine},
  pages = {149--163},
  year = 	 2010,
  month = jun,
  URL = {https://www.irit.fr/~Martin.Strecker/Publications/afadl10.html},
}