Basic Paramodulation and Superposition

We introduce a class of restrictions for the ordered paramodulation and \u000Asuperposition calculi (inspired by the ıt basic\/ strategy for narrowing), \u000Ain which paramodulation inferences are forbidden at terms introduced by \u000Asubstitutions from previous inference steps. These refinements are compatible \u000Awith standard ordering restrictions and are complete without paramodulation \u000Ainto variables or using functional reflexivity axioms. We prove refutational \u000Acompleteness in the context of deletion rules, such as simplification by \u000Arewriting (demodulation) and subsumption, and of techniques for eliminating \u000Aredundant inferences. Finally, we discuss experimental data obtained both from \u000Aa modification of Otter and from our prototype Lisp implementation