up: Publications |
Abstract |
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 = {http://www.irit.fr/~Martin.Strecker/Publications/afadl10.html}, }
Last modified: Fri May 14 15:21:49 CEST 2010 |