Basic Paramodulation
Citations Over TimeTop 1% of 1995 papers
Abstract
We introduce a class of restrictions for the ordered paramodulation and superposition calculi (inspired by the basic strategy for narrowing), which forbid paramodulation inferences at terms introduced by substitutions from previous inference steps. In addition we introduce restrictions based on term selection rules and redex orderings, which are general criteria for delimiting the terms which are available for inferences. 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.
Related Papers
- → On interreduction of semi-complete term rewriting systems(2001)7 cited
- Persistence of Termination for Term Rewriting Systems with Ordered Sorts(2005)
- → Extending Context-Sensitivity in Term Rewriting(2010)2 cited
- → Axioms vs. rewrite rules: from completeness to cut elimination(2023)