Reasoning about knowledge by variable forgetting
Kaile Su, Guanfeng Lv, Yan Zhang · 2004
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.