Kaile Su, Guanfeng Lv, and Yan Zhang
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 and a set of observable variables for an agent, we show that the notion of agent knowing a formula can be defined as a weakest sufficient condition of the formula on the set of observable variables for the agent under background knowledge base. 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.