Intelligent systems have various kinds of representational needs to be used in real world. To support multiple representational formalisms and specialized reasoning for each formalism in a well-defined and precise way, a new strategy called hybrid systems for knowledge representation has been studied.
In this thesis, a new method for hybrid knowledge representation is developed by integrating frames and Horn clauses. A hybrid system called Sphinx is also developed on the basis of this formalism. Sphinx is a theorem prover-based hybrid system of which proof mechanism is a SLD-resolution strategy augmented with a special-purpose inference system for frame-based descriptions. From systematic point of view, Sphinx also consists of two major components for terminological and assertional reasoning.
It is also shown that Horn clause can be combined efficiency with the conventional frame-based description system if some useful assumptions are given. By integrating theses two kinds of reasoners, more expressive power and deductive capability than simple database-style hybrid systems can be offered, while retaining the reasoning efficiency.
To reflect the terminological knowledge completely in proving a query, deduction rules are included automatically in the ABox and an extended logical query language involving explicit logical connectives and quantifiers is designed. An efficient and sound query evaluation procedure with domain closure assumption and the notion of complete knowledge base is also presented.
To permit incremental additions and retractions of factual knowledge, a new truth maintenance strategy is presented in this thesis. The truth maintenance strategy uses semantic dependencies of predicates by referring the TBox. With this approach, it is shown that even a theorem prover-based hybrid systems can support the dynamic revision of knowledge. It is also ascertained that the use of the negation-as-failure rule can simplify greatly the query processing and truth maintenance process.
인공 지능 시스템들이 실제 응용 분야에서 적용되기 위해서는 많은 종류의 지식 표현 기법들이 필요하다. 여러 종류의 표현 기법이나, 특수 목적의 추론 기법들을 분명하고 잘 정립된 의미론을 바탕으로 동시에 제공하기 위한 새로운 기법이 혼성 지식 표현 방식이다.
이 논문에서는 틀과 혼 (Horn) 논리절을 결합한 새로운 방식의 혼성 지식 표현 기법을 제안하고 있다. 또한, 이러한 형식에 바탕을 둔 Sphinx라는 시스템을 개발하였다. Sphinx는 SLD 레졸루션을 틀에 바탕을 둔 시스템과 결합하여 추론 하도록 확장한 증명 기법에 바탕을 둔 혼성 시스템이다. 시스템 구성의 관점에서 보면, Sphinx 역시 다른 시스템과 마찬가지로 용어적 추론을 다루는 부분과 단정적 지식과 추론을 다루는 두개의 큰 부분으로 이루어 진다.
이 논문에서는 혼 논리절이 일반적이틀 시스템하고 어떤 가정이 이루어지면 효과적으로 결합할 수 있는 가를 보이고 있다. 즉, 영역 닫힘 가정, 실패에 의한 거짓 추론, 완전 지식 베이스 개념들이 어떻게 두 기법의 결합을 효과적으로 하는 가를 보이고 있다. 이 두가지 기법을 결합함으로써, 단순 데이타베이스 형식의 혼성 시스템 보다 뛰어난 표현력과 연역 기능을 갖추게 된다. 또한 이 방식은 혼 논리절이 갖고 있는 추론의 효율성을 그대로 유지 할 수 있다.
Sphinx는 기본적으로 지적인 질의응답 시스템을 구성하는데 보다 효과적이다. 질의를 증명하는 과정에서는 용어적 지식과 추론을 반영해야 하는데, 이를 위해 연역 규칙이 자동으로 생성되도록 하였으며, 질의 언어를 논리 연결사나 한정자를 포함하도록 일반화하였다. 또한, 효과적이고 정당한 질의 처리 방식을 개발하였다.
지식 표현 시스템이 단순한 정리 증명기가 아니기 위해서는 동적인 지식의 변화가 허용되어야 한다. Sphinx는 단순 사실인 경우에 한하여, 이와 같은 지식의 변경이 허용되도록 하였으며, 이 방식은 혼성 지식 표현 방식의 특성을 최대한 이용한 방식이다. 나아가서, 실패에 의한 거짓 추론 방식이 진리 유지를 얼마나 단순하게 처리할 수 있도록 하는 가를 보이고 있다.