タイトル | The Role of Reformulation in the Automatic Design of Satisfiability Procedures |
本文(外部サイト) | http://hdl.handle.net/2060/19960047165 |
著者(英) | VanBaalen, Jeffrey |
著者所属(英) | Wyoming Univ. |
発行日 | 1992-04-01 |
言語 | eng |
内容記述 | Recently there has been increasing interest in the problem of knowledge compilation (Selman & Kautz91). This is the problem of identifying tractable techniques for determining the consequences of a knowledge base. We have developed and implemented a technique, called DRAT, that given a theory, i.e., a collection of firstorder clauses, can often produce a type of decision procedure for that theory that can be used in the place of a general-purpose first-order theorem prover for determining many of the consequences of that theory. Hence, DRAT does a type of knowledge compilation. Central to the DRAT technique is a type of reformulation in which a problem's clauses are restated in terms of different nonlogical symbols. The reformulation is isomorphic in the sense that it does not change the semantics of a problem. |
NASA分類 | Cybernetics |
レポートNO | 96N32927 |
権利 | No Copyright |
URI | https://repository.exst.jaxa.jp/dspace/handle/a-is/103355 |
|