Item

Abstract

We propose inference systems based on ordered chaining and a concept of
(global) redundancy for clauses and inferences for dealing with total
orderings. A key to the practicality of chaining techniques is the extent to
which so-called variable chainings can be restricted. We demonstrate that
ordering restrictions and the rewrite techniques which account for their
completeness considerably restrict variable chaining. For dense total orderings
we show that the techniques for eliminating unshielded variables are admissible
simplifications so that no variable chaining is needed at all. We also include
equality by combining ordered chaining with superposition.