Logical reasoning of theorem proving is the key to solving many other puzzles, to solving problems in mathematics, to designing electronic circuits, to verifying programs, and answering many everyday questions. Since the first-order predicate logic is generally sufficient for mathematical reasoning and offers the advantage of being partially decidable, it is widely used in automated reasoning. There have been considerable efforts in developing partial decision procedures of the first-order predicate logic. Notable among them is the resolution method, which is very powerful but relatively slow. Since the introduction of the resolution method by Robinson, many refinements have been proposed to increase the efficiency. One of them is the connection graph proof procedure. The connection graph proof procedure has some distinct advantages over the previous approaches based upon resolution. But the connection graph proof procedure has some problems in applying subsumption rule and in parallelizing the proof procedure, with which we are concerned.
Subsumption is a strong tool for reducing the search in proof procedure. But the logical consistency of proof procedure is not preserved when the subsumption rule is used in connection graph proof procedure. To maintain the logical consistency, we define a new $\theta$-subsumption by considering the implicit constraints imposed by links. Since the new definition of $\theta$-subsumption is restrictive, there may exist some clauses which are subsumed with the original definition of $\theta$-subsumption but not with the new definition. Hence, we provide a graph transformation method which makes C subsume D with the new definition if C subsumes D with the original definition.
The subsumption test must be repeated very often and thus its efficiency is decisive for its use. There have been several researches to overcome the expensiveness of subsumption. One of them is the s-link test, in which it is essential to find a set of pairwise strongly compatible matching substitutions between literals in two clauses. We present an algorithm for the s-link test which is based on both the reduction of possible matching substitutions and appropriate bit operations. The worst-case time complexity of this algorithm is analyzed in terms of the estimated maximal number of string comparison and it is shown that our complexity is lower than the other algorithms based on the s-like test.
In exploiting parallelism, we can take advantages of the connection graph proof procedure. However, parallelism with no restriction may cause the missing link problem and thus results in the logical inconsistency. The missing link problem can be solved by use of restrictive selection method or deadlock detection and resolving method. But, these approaches may reduce parallelism and thus no benefit may be obtained by parallelizing proof procedure in some cases. We propose a new solution to the missing link problem, in which each process partially detects and recovers missing links and all missing links are recovered consequently by the co-works between processes.
The AND-parallelism has the advantage of taking larger deduction steps than a link resolution does. Also, it has high potential of parallelism. In AND-parallelism, all the links connecting literals in a clause are resolved concurrently. The major step in AND-parallelism is to find all solution unifiers from the given set of mgu's. All solution unifiers can be obtained by getting all combinations of mgu's and checking for consistency and obtaining the solution unifiers for all consistent combinations. However, this method is inefficient because it wastes so much time to find solution unifiers of combinations of mgu's which have no solution unifier. We improve the algorithm for calculating all solution unifiers of a clause by singling out the combinations of mgu's which have no solution unifier.
Based on the new subsumption method, the new solution to the missing link problem, and the refined AND-parallelism we suggest a new parallel proof procedure using several parallelism in combined form, and show that the proposed proof procedure has better performance than other proof procedure using single parallelism.
논리적 추론 (또는 정리 증명)은 퍼줄 문제 해결, 수학문제 해결, 전자회로 설계, 프로그램 정확성 검증 및 지식 기반 시스템 등 에서 핵심적 역할을 담당한다. 일차 술어 논리는 표현력이 좋고 준결정적인 추론 방법을 제공하기 때문에 정리 증명 분야에서 널리 사용되고 있다. 지금까지 일차 술어 논리에 바탕을 둔 여러 추론 방법이 제안되어 있는데, 이 중 융합 방법(resolution method) 이 가장 널리 이용되고 있다 융합 방법은 하나의 규칙을 이용하여 강력한 추론 능력을 제공하기 때문에 현재 많은 정리 증명기가 이에 바탕을 두고 있으나 추론 속도가 비교적 느린 문제점을 갖고 있다. 융합 방법의 추론 속도를 개선하기 위해 많은 방법들이 제안되어 왔는데, 이중 대표적인 방법이 연결 그래프에 바탕을 둔 정리 증명 방법이다. 연결 그래프에 바탕을 둔 정리 증명 방법은 다른 방법에 비해 많은 장점을 갖고 있지만 피포함절 제거 규칙 적용시 문제점과 병렬화시 문제점들을 갖고 있다. 본 논문은 이러한 문제점들을 해결하고 이를 바탕으로 효율적인 새로운 정리 증명법을 제시하는데 그 목적이 있다.
피포함절 제거 규칙은 중복된 정보를 제거하는 규칙으로 여러 정리 증명 방법에서 추론 속도를 향상시키기 위하여 사용하고 있다. 이런 규칙이 연결 그래프에 바탕을 둔 정리 증명 방법에 사용될 경우 논리적 불일치가 발생하여 옳지 않는 추론을 할 수 있다. 본 논문에서는 이 문제점을 해결하기 위해 연결그래프의 특성을 고려한 새로운 피포함절 제거 규칙을 제시하였고 이 새로운 규칙을 사용할 경우 논리적 불일치가 발생하지 않음을 증명하였다. 또한, 포함 관계를 효율적으로 검사할 수 있는 새로운 방법을 제시하였고 이 방법이 기존의 방법에 비해 효율적임을 보였다.
연결 그래프에 바탕을 둔 정리 증명 방법은 그래프에 바탕을 두고 있어 병렬성을 추구하기가 용이하나 무제한적으로 병렬성을 추구할 경우 필요한 정보의 손실로 인해 논리적 불일치가 발생한다. 이 문제점을 해결하기 위해 병렬성에 제약을 가하는 방법들이 제안되었는데, 본 논문에서는 병렬성에 제약을 가하지 않고 이 문제점을 해결하는 방법을 제시하고 이 방법의 정확성을 증명하였다.
연결 그래프에 바탕을 둔 정리 방법의 속도를 개선하기 위해 다양한 병렬성 들이 추구되고 있는데, 이 중 AND-병렬성은 병렬성이 높고 한번에 많은 추론을 할 수 있다는 장점 때문에 많은 연구들이 이루어지고 있다. 그러나 AND-병렬성은 공유 변수에 의한 문제점으로 다른 병렬성에 비해 추론 과정이 복잡해지는데 본 논문에서는 가장 시간이 많이 소요되는 부분을 개선함으로써 AND-병렬성을 이용한 정리 증명 방법을 개선하였다.
결과적으로, 본 논문에서는 위에서 제시한 방법들을 이용하여 새로운 병렬성, 즉 혼합 병렬성을 이용한 정리 증명 방법을 제시하였고 시뮬레이션을 통하여 이의 효율성을 입증하였다.
