Loading...
Please wait, while we are loading the content...
Similar Documents
The role of reformulation in the automatic design of satisfiability procedures
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | VanBaalen, Jeffrey |
| Copyright Year | 1992 |
| Description | 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. |
| File Size | 1051347 |
| Page Count | 12 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_19960047165 |
| Archival Resource Key | ark:/13960/t9z082076 |
| Language | English |
| Publisher Date | 1992-04-01 |
| Access Restriction | Open |
| Subject Keyword | Cybernetics Expert Systems Knowledge Based Systems Semantics Artificial Intelligence Theorem Proving Knowledge Representation Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Article |
