Reasoning about Knowledge by Variable Forgetting

In this paper, we investigate knowledge reasoning within a simple framework called knowledge structure. We use variable forgetting as a basic operation for one agent to reason about its own or other agents' knowledge. In our framework, two notions namely agents' observable variables and the weakest sufficient condition play important roles in knowledge reasoning. Given a background knowledge base T and a set of observable variables Oi for each agent i, we show that the notion of agent i knowing a formula ϕ can be defined as a weakest sufficient condition of ϕ on Oi under T. Moreover, we show how to capture the notion of common knowledge by using a generalized notion of weakest sufficient condition. We also discuss possible applications of our framework in some interesting domains such as the automated analysis of the well-known muddy children puzzle and the verification of the revised Needham-Schroeder protocol.