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

Cited 0 time in webofscience Cited 0 time in scopus
  • Hit : 500
  • Download : 0
DC FieldValueLanguage
dc.contributor.advisorCho, Jung-Wan-
dc.contributor.advisor조정완-
dc.contributor.authorKim, Byeong-Man-
dc.contributor.author김병만-
dc.date.accessioned2011-12-13T05:21:52Z-
dc.date.available2011-12-13T05:21:52Z-
dc.date.issued1992-
dc.identifier.urihttp://library.kaist.ac.kr/search/detail/view.do?bibCtrlNo=60520&flag=dissertation-
dc.identifier.urihttp://hdl.handle.net/10203/32934-
dc.description학위논문(박사) - 한국과학기술원 : 전산학과, 1992.8, [ [viii], 114 p. ]-
dc.description.abstractLogical 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...eng
dc.languageeng-
dc.publisher한국과학기술원-
dc.title(A) parallel connection graph proof procedure using hybrid parallelism-
dc.title.alternative혼성 병렬성을 이용한 정리 증명 방법-
dc.typeThesis(Ph.D)-
dc.identifier.CNRN60520/325007-
dc.description.department한국과학기술원 : 전산학과, -
dc.identifier.uid000875062-
dc.contributor.localauthorCho, Jung-Wan-
dc.contributor.localauthor조정완-
Appears in Collection
CS-Theses_Ph.D.(박사논문)
Files in This Item
There are no files associated with this item.

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0