Reasoning about Relations with Dependent Types: Application to Context-Aware Applications

Abstract : Generally, ontological relations are modeled using fragments of first order logic (FOL) and difficulties arise when meta-reasoning is done over ontological properties, leading to reason outside the logic. Moreover, when such systems are used to reason about knowledge and meta-knowledge, classical languages are not able to cope with different levels of abstraction in a clear and simple way. In order to address these problems, we suggest a formal framework using a dependent (higher order) type theory. It maximizes the expressiveness while preserving decidability of type checking and results in a coherent theory. Two examples of meta-reasoning with transitivity and distributivity and a case study illustrate this approach.
Type de document :
Communication dans un congrès
J. Rauch and Z. W. Ras and P. Berka and T. Elomaa. ISMIS 2009, Sep 2009, Prague, Czech Republic. Springer Berlin / Heidelberg, 5722, pp.171-180, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-04125-9_20〉
Liste complète des métadonnées

http://hal.univ-smb.fr/hal-00498210
Contributeur : Richard Dapoigny <>
Soumis le : mardi 6 juillet 2010 - 23:54:10
Dernière modification le : mercredi 10 janvier 2018 - 09:48:55

Identifiants

Collections

UGA

Citation

Richard Dapoigny, Patrick Barlatier. Reasoning about Relations with Dependent Types: Application to Context-Aware Applications. J. Rauch and Z. W. Ras and P. Berka and T. Elomaa. ISMIS 2009, Sep 2009, Prague, Czech Republic. Springer Berlin / Heidelberg, 5722, pp.171-180, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-04125-9_20〉. 〈hal-00498210〉

Partager

Métriques

Consultations de la notice

42