Mechanizing Local Reasoning with Contexts

One of the main problems in formalizing common sense reasoning is that often its conclusions rely on partial information. Although this may depend on a lack of information, most times it depends on the fact that (common sense) reasoning is ‘local’, i.e. does not use all the potentially available knowledge when drawing a conclusion. In [BG95], local reasoning is formalized in a multi context framework. In the proposed architecture, subsets of a knowledge base are used to formulate local theories for given problems. In this paper, we address the problem of mechanizing the conceptual architecture. We focus on the mechanization of the basic mechanism for the formulation of local theories, and in particular on the process of ‘lifting’ the information of a context into another context. As a case study, we describe the mechanization McCarthy’s Glasgow-London-Moscow proble