Goal Reasoning with Context Record Types

摘要

The concept of goal is central in Artificial Intelligence and its modelling is a challenging issue. It has been given much attention in areas such as Requirement Engineering (RE) and Planning and Scheduling, where its modelling can support formal reasoning through goal types, goal attributes and relations to other components. However there is a lack of formalisms able to reason with goal structures in dynamic environments. We claim that a logical framework based on Intuitionistic Type Theory and more precisely, on Dependent Record Types is able to address this problem. The formal foundations rely on context modelling through dependent record types allowing partial knowledge and dynamic reasoning. For the purpose of goal modelling, we introduce a family of functions which map Context Record Types to Intentional Record Types expressing their related actions and goals. A case study in planning illustrates this approach.