Maximal strategies for paramodulation with non-monotonic orderings

A west ordering is a well-founded (strict partial) ordering on terms that satisfies the subterm property. In [Bofill, Godoy, Nieuwenhuis, Rubio, (BGNR-LICS99)] the completeness of an ordered paramodulation inference system w.r.t. west orderings was proved, thus dropping for the first time the monotonicity requirements on the ordering. However, the inference system still required the eager selection of negative equations. Here we improve upon [BGNR-LICS99] in two directions. On the one hand, we show that the results are compatible with constraint inheritance and the so-called basic strategy [(Bachmair, Ganzinger, Lynch, Snyder (1995IC)), (Nieuwenhuis, Rubio (1995JSC))], thus further restricting the search space. On the other hand, we introduce an inference system where also the positive equations of non-unit clauses can be selected, provided that they are maximal