非表示:
キーワード:
-
要旨:
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.
