Towards Ontological Correctness of Part-whole Relations with Dependent Types - Université Savoie Mont Blanc Access content directly
Conference Papers Year : 2010

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.
No file

Dates and versions

hal-00498191 , version 1 (06-07-2010)

Identifiers

  • HAL Id : hal-00498191 , version 1

Cite

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. ⟨hal-00498191⟩
119 View
0 Download

Share

Gmail Mastodon Facebook X LinkedIn More