Towards a Conceptual Structure based on Type Theory.
Richard Dapoigny, Patrick Barlatier · 2008
Abstract. Since a conceptual structure is a typed system it is worthwhile to investigate how a type theory can serve as a basis to reason about concepts and relations. In this article, we look at this issue from a proof-theoretical perspective using the constructive (or intuitionistic) logic and the Curry-Howard correspondence. The resulting constructive type theory introduces Dependent Record Types (DRT) which offers a conceptual structure with a simple and natural representation. The crucial aspect of the proposed typed system is its decidability while maintaining a high level of expressivity. 1