知识推理中的变量遗忘
Variable Forgetting in Reasoning about Knowledge
摘要：
在本文中，我们研究知识推理的一个简单的框架内称为知识结构。我们使用变量遗忘作为一个代理的基本操作，以推理自己或其他代理的知识。在我们的框架中，两个概念，即主体\可观察变量和最弱充分条件发挥了重要作用的知识推理。给定一个背景知识基和一组可观测变量，我们证明了在背景知识基下，智能体知道一个公式的概念可以定义为该公式的一个最弱充分条件.此外，我们展示了如何捕捉的概念，共同知识，使用广义的概念，最弱的充分条件。此外，我们表明，公告运营商可以方便地处理通过我们的知识结构的概念。此外，我们探讨了计算复杂性的问题是否认识公式实现的知识结构。在一般情况下，这个问题是PSPACE困难的;然而，对于一些有趣的子情况，它可以简化为co-NP。最后，我们讨论了我们的框架可能的应用在一些有趣的领域，如著名的泥泞的儿童难题的自动化分析和验证修订后的Needham-Schroeder协议。我们相信，在许多情况下，有关知识的可用信息的自然呈现是以知识结构的形式进行的。与相应的多智能体S5 Kripke结构相比，它的价值在于它可以更加简洁。
英文摘要：
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 each agent, we show that the notion of an agent knowing a formula can be defined as a weakest sufficient condition of the formula under background knowledge base. Moreover, we show how to capture the notion of common knowledge by using a generalized notion of weakest sufficient condition. Also, we show that public announcement operator can be conveniently dealt with via our notion of knowledge structure. Further, we explore the computational complexity of the problem whether an epistemic formula is realized in a knowledge structure. In the general case, this problem is PSPACE-hard; however, for some interesting subcases, it can be reduced to co-NP. Finally, we 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. We believe that there are many scenarios where the natural presentation of the available information about knowledge is under the form of a knowledge structure. What makes it valuable compared with the corresponding multi-agent S5 Kripke structure is that it can be much more succinct.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
