- Logical reasoning of theorem proving is the key to solving many other puzzles, to solving problems in mathenatics, 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 precedure. The connection graph proof procedure has some distinct advantages over the previous approaches based upon resolution. But the conection 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 defintion. 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 bave 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 pairwis...

- Advisors
- Cho, Jung-Wan
*researcher*; 조정완*researcher*

- Publisher
- 한국과학기술원

- Issue Date
- 1992

- Identifier
- 60520/325007 / 000875062

- Language
- eng

- Description
학위논문(박사) - 한국과학기술원 : 전산학과, 1992.8, [ [viii], 114 p. ]

- Appears in Collection
- CS-Theses_Ph.D.(박사논문)

- Files in This Item
- There are no files associated with this item.

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.