In the last years, epistemology, the study of knowledge and belief, began to attract growing interest in many domains such as economics, linguistics, artificial intelligence, and computer science. As a result, it had become necessary to develop a well-formalized tool to describe each agent's knowledge and belief, and epistemic logics, either modal logical forms or first-order logical forms, have been used for this purpose. For the semantics of epistemic logics, two different models have been used: one is the classical possible-worlds model, and the other is the more recent deduction model. In the possible-worlds model, a set of pre-assumed possible worlds exists, and each agent's knowledge and belief are represented by accessibility relations between possible worlds. The characteristics of knowledge and belief can be given by restricting these accessibility relations. Possible-worlds model is in itself very simple, and natural in the point of man, but as it overidealizes the situation, it suffers from the famous problem, logical omniscience, that every agent knows or believes all logically valid formulas and all logical consequences. In the real world, this logically omniscient agent cannot exist, even though his inferential power is complete, as the resources he can use are very limited. On the other hand, deduction model assumes that each agent has a belief system, each of which is composed of base beliefs and deduction rules. Each agent's knowledge and belief are represented by set-element relations for the belief system. As deduction model does not prescribe the inference power, it does not suffer from the logical omniscience, but it has weakness to formalize some important characteristics of knowledge and belief, such as introspectiveness. In this paper, we propose a new semantics for epistemic logics, called box model. It is designed to model real agents like deduction model, but it can handle various characteristics of knowledge and belief like possible-worlds model. It can also handle agent modelling informations, which are necessary in modelling knowledge or belief for other agents. We analyzed the characteristics of our model, and compared them with other models. We also propose proof mechanisms for epistemic modal logics based on box model. As in deduction model, we develop a resolution method which is similar to B-resolution. As this resolution method is very inefficient, we also develop a more efficient proof mechanism using structures called view, which was first used in deduction model. As an application of our model, we develop a knowledge and belief representation system for multi-agents called Makers. Makers can represent and reason about multi-agent's knowledge and belief as well as the factual knowledge of the actual world. It can also process some axioms which are usually used to represent characteristics of each agent's knowledge and belief. Makers can be used as a tool to construct knowledge bases for various applications where multi-agents co-exist, and some sample knowledge bases are constructed to demonstrate its usefulness and practicality.
고대 철학에서부터 시작한 믿음과 지식에 관한 연구는 최근 전산학 분야는 물론 경제학, 철학, 수학 분야등 여러 분야에서 폭넓게 연구되고 있다. 믿음과 지식에 대한 모형으로는 철학에서 만들어진 가능 세계 모형이사용되어 왔으나 믿음과 지식을 가진 에이젼트가 논리적으로 전능해야한다는 문제점을 갖고 있다. 이와 같은 문제점을 해결하기 위해 만들어진 것이 추론 모형이나 이는 다른 에이젼트에 대한 지식이나 믿음을 나타낼 수 없는 문제점이 있다. 따라서 본 논문에서는 믿음과 지식에 대한 새 모형으로 상자 모형을 제안하였다. 상자 모형은 추론 모형을 확장한 것으로 가능 세계 모형과 같은 논리적 전능의 문제가 발생하지 않으며 실제 세계의 에이젼트를 나타낼 수 있다. 또 추론 모형과는 달리 다른 에이젼트의 믿음이나 지식, 추론 규칙과 같은 에이젼트 모델링에 대한 정보도 나타낼 수 있다. 또 새로 제안된 상자 모형을 기초로한 증명 방법도 설계하였다. 기존의 증명 방법들은 에이젼트의 특성에 따라 증명 방식이 바뀌어야 하지만 특정 규칙 내에서는 이를 바꾸지 않고 그대로 사용할 수 있는 통일된 증명 방법을 개발하였다. 이를 위해 먼저 B-resolution과 유사한 resolution 방법을 개발하였으며 보다 더 효율적인 View 구조를 이용한 증명 방법도 개발하였다. 또 개발된 증명 방법의 완전성과 정당성도 증명하였다. 본 논문에서 제안한 모형의 한 응용 분야로 다중 에이젼트의 믿음과 지식을 표현할 수 있는 Makers라는 믿음과 지식 표현 시스템을 설계하였다. 이는 기존의 지식 표현 시스템과는 달리 여러 에이젼트의 지식과 믿음과 표현할 수 있으며 다른 에이젼트의 지식이나 믿음에 대한 추론도 가능하다. 또 각 에이젼트는 여러가지 다른 특성을 가질 수 있으며 그 특성에 따라 추론할 수 있다. Makers 의 유용성을 보이기 위해 몇가지 지식 베이스를 구축하였다.