Abstract:
|
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. |