Name
Abstract | ||
|---|---|---|
A refinement of paramodulation, called hyperparamodulation, is the focus of attention in this paper. Clauses obtained by the use of this inference rule are, in effect, the result of a sequence of paramodulations into one common nucleus. Among the interesting properties of hyperparamodulation are: first, clauses are chosen from among the input and designated as nuclei or "into" clauses for paramodulation; second, terms in the nucleus are starred to restrict the domain of generalized equality substitution; third, total control is thus iteratively established over all possible targets for paramodulation during the entire run of the theorem-proving program; and fourth, application of demodulation is suspended until the hyperparamodulant is completed. In contrast to these four properties which are reminiscent of the spirit of hyper-resolution, the following differences exist: first, the nucleus and the starred terms therein, which are analogous to negative literals, are determined by the user rather than by syntax; second, nuclei are not restricted to being mixed clauses; and third, while hyper-resolution requires inferred clauses to be positive, no corresponding requirement exists for clauses inferred by hyperparamodulation. |
Year | DOI | Venue |
|---|---|---|
1980 | 10.1007/3-540-10009-1_17 | CADE |
Keywords | Field | DocType |
theorem proving,inference rule,quantum mechanics | Discrete mathematics,Algorithm,Syntax,Rule of inference,Mathematics,Mathematical logic | Conference |
ISBN | Citations | PageRank |
3-540-10009-1 | 18 | 2.90 |
References | Authors | |
3 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Larry Wos | 1 | 450 | 92.39 |
| Ross A. Overbeek | 2 | 760 | 234.40 |
| Lawrence J. Henschen | 3 | 478 | 280.94 |