Formalizing Context in Intuitionistic Type Theory

Article type: Research Article

Authors: Boldini, Pascal

Affiliations: CAMS, Équipe LaLIC, ISHA, Université Paris IV, PARIS, FRANCE. Pascal.Boldini@paris4.sorbonne.fr

Note: [] Address for correspondence: CAMS, Équipe LaLIC, ISHA, Université Paris IV, PARIS, FRANCE

Abstract: The article discusses formal aspects of the notion of context as needed in AI applications. We advocate the use of Martin-Löf's intuitionistic type theory to formalize and implement contexts. Through many examples belonging to the domains of computational semantics and knowledge based systems, we show that the built-in notion of context in intuitionistic type theory is a structure rich enough for representing most of the features that characterize contexts in an AI perspective. The fact that many recent theorem provers are built on the different theories of types suggests new perspectives in the development of AI applications.

Keywords: Artificial Intelligence, Contexts, Type Theory, Natural Language Processing, Knowledge Based Systems, Situations

DOI: 10.3233/FI-2000-42201

Journal: Fundamenta Informaticae, vol. 42, no. 2, pp. 105-127, 2000