Affiliations: LISTIC/Polytech'Savoie, University of Savoie, Po. Box 80439, 74944 Annecy-le-vieux cedex, France. [email protected], [email protected]
Note: [] Address for correspondence: LISTIC/Polytech'Savoie, Domaine Universitaire Po. Box 80439, 74944 Annecy le vieux cedex, France
Abstract: In the area of knowledge representation, a challenging topic is the formalization of context knowledge on the basis of logical foundations and ontological semantics. However, most attempts to provide a formal model of contexts suffer from a number of difficulties, such as limited expressiveness of representation, restricted variable quantification, lack of (meta) reasoning about properties, etc. In addition, type theory originally developed for formal modeling of mathematics has also been successfully applied to the correct specification of programs and in the semantics of natural language. In this paper, we suggest a type theoretical approach to the problem of context and action modeling. Type theory is used both for representing the system's knowledge of the discourse domain and for reasoning about it. For that purpose, we extend an existing dependent type theory having nice properties, with context-based rules and appropriate inductive types. We claim that the resulting theory exploiting the power of dependent types is able to provide a very expressive system together with a unified theory allowing higher-order reasoning.
Keywords: Context, Action, Type Theory, Dependent Types, Subtyping, Subsumption, Partonomies
