| タイトル | 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 |
|
