Vers un modèle formel pour le raisonnement à partir des contextes
Ces dix dernières années de nombreuses recherches dans le domaine des contextes ont été menées, cependant, peu d'entre elles ont utilisé la logique comme sémantique. Dans cet article, nous abordons ce problème en utilisant une théorie constructive des types comme support pour la modélisation des contextes. Nous décrivons un outil théorique formé à partir de la théorie intuitionniste des types. Cette théorie est étendue par les enregistrements à types dépendants DTR qui permettent la représentation de connaissances partielles et le raisonnement sur des données évolutives.
In the last decade, there has been much interest in the development of contextaware systems but few logic-based formal theories of contexts have emerged. In this article, we look at this issue from a proof-theoretical perspective and we describe a type-theoretical framework for reasoning about contexts. The use of constructive type theory with Dependently Typed Records (DTR) allows for a partial knowledge and dynamic reasoning to take place while assuming an Open World Assumption.
R.DAPOIGNY, P.BARLATIER
théorie constructive des types, intuitionisme, enregistrements à types dépendants, sous-typage, causalité, vérification de types, ontologies de domaine.
constructive type theory, intuitionism, dependent record types, sub-typing, causality, type-checking, domain ontologies.
Français
|
