BASIC PARAMODULATION

We introduce a class of restrictions for the ordered paramodulation an d superposition calculi (inspired by the basic strategy for narrowing) , which forbid paramodulation inferences at terms introduced by substi tutions from previous inference steps. In addition we introduce restri ctions based on term selection rules and redex orderings, which are ge neral criteria for delimiting the terms which are available for infere nces. These refinements are compatible with standard ordering restrict ions and are complete without paramodulation into variables or using f unctional reflexivity axioms. We prove refutational completeness in th e context of deletion rules, such as simplification by rewriting (demo dulation) and subsumption, and of techniques for eliminating redundant inferences. (C) 1995 Academic Press, Inc.