Name
Abstract | ||
|---|---|---|
We introduce a class of restrictions for the ordered paramodulation and superposition calculi (inspired by the basic strategy for narrowing), in which paramodulation inferences are forbidden at terms introduced by substitutions from previous inference steps. These refinements are compatible with standard ordering restrictions and are complete without paramodulation into variables or using functional reflexivity axioms. We prove refutational completeness in the context of deletion rules, such as simplification by rewriting (demodulation) and subsumption, and of techniques for eliminating redundant inferences. Finally, we discuss experimental data obtained from a modification of Otter. |
Year | DOI | Venue |
|---|---|---|
1992 | 10.1007/3-540-55602-8_185 | CADE |
Keywords | Field | DocType |
basic paramodulation | Demodulation,Superposition principle,Algebra,Experimental data,Inference,Axiom,Computer science,Algorithm,Rewriting,Completeness (statistics),Rule of inference | Conference |
Volume | ISBN | Citations |
607 | 3-540-55602-8 | 59 |
PageRank | References | Authors |
7.59 | 14 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Leo Bachmair | 1 | 1006 | 90.72 |
| Harald Ganzinger | 2 | 1513 | 155.21 |
| Christopher Lynch | 3 | 166 | 25.33 |
| Wayne Snyder | 4 | 225 | 23.79 |