(A) parallel connection graph proof procedure using hybrid parallelism = 혼성 병렬성을 이용한 정리 증명 방법

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-Wanresearcher조정완researcher
Publisher
한국과학기술원
Issue Date
1992
Identifier
60520/325007 / 000875062
Language
eng
Description

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

URI
http://hdl.handle.net/10203/32934
Link
http://library.kaist.ac.kr/search/detail/view.do?bibCtrlNo=60520&flag=t
Appears in Collection
CS-Theses_Ph.D.(박사논문)
Files in This Item
There are no files associated with this item.
  • Hit : 118
  • Download : 0
  • Cited 0 times in thomson ci

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0