Towards Ontological Correctness of Part-whole Relations with Dependent Types

Abstract : Generally, part-whole relations are modeled using fragments of first-order logic(FOL) and difficulties arise when meta-reasoning is done over their properties, leading to reason outside the logic. Alternatively, classical languages for ontological reasoning such as Description Logics + Logic Programming lack of expressive formal foundations resulting in ambiguous interpretations of relations. Moreover, they show some difficulties to prove that a given meta property is logically correct. In order to address these problems, we suggest a formal framework using a dependent (higher-order) type theory such as those used in program checking and theorem provers (e.g., Coq). All properties of part-whole relations are formalized through abstract constructs called parameterized specifications (p-specifications). We detail their content and explain how they are suitable to build an ontology of formal properties that can be further used for reasoning about higher-order properties.
Type de document :
Communication dans un congrès
Proceedings of the Sixth international Conference on Formal ontology in information Systems (FOIS 2010), May 2010, Toronto, Canada. pp. 45-58, 2010
Liste complète des métadonnées

http://hal.univ-smb.fr/hal-00498191
Contributeur : Richard Dapoigny <>
Soumis le : mardi 6 juillet 2010 - 22:43:13
Dernière modification le : mercredi 10 janvier 2018 - 09:49:55

Identifiants

  • HAL Id : hal-00498191, version 1

Collections

UGA

Citation

Richard Dapoigny, Patrick Barlatier. Towards Ontological Correctness of Part-whole Relations with Dependent Types. Proceedings of the Sixth international Conference on Formal ontology in information Systems (FOIS 2010), May 2010, Toronto, Canada. pp. 45-58, 2010. 〈hal-00498191〉

Partager

Métriques

Consultations de la notice

284