Name
Abstract | ||
|---|---|---|
Over the past 25 years, researchers have written numerous deduction systems based on resolution and paramodulation. Of these systems, very few have been capable of generating and maintaining aformula database containing more than just a few thousand clauses. These few systems were used to explore mechanisms for rapidly extracting limited subsets of ‘relevant’ clauses. We have developed a simple, powerful deduction system that reflects some of the best of the ideas that have emerged from the research. This paper describes that deduction system and casts the idea in a form that makes them easily accessible to researchers wishing to write their own high-performance systems. |
Year | DOI | Venue |
|---|---|---|
1994 | 10.1007/BF00881885 | J. Autom. Reasoning |
Keywords | Field | DocType |
Resolution/paramodulation systems,formula database,deduction system | Computer science,Algorithm,Database | Journal |
Volume | Issue | ISSN |
12 | 2 | 0168-7433 |
Citations | PageRank | References |
3 | 0.68 | 3 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ralph M. Butler | 1 | 188 | 11.39 |
| Ross A. Overbeek | 2 | 760 | 234.40 |