非表示:
キーワード:
-
要旨:
We design new inference systems for total orderings
by applying rewrite techniques to chaining calculi.
Equality relations may either be specified axiomatically
or built into the deductive calculus via paramodulation or superposition.
We demonstrate that our inference systems are compatible
with a concept of (global) redundancy for clauses and inferences
that covers such widely used simplification techniques
as tautology deletion, subsumption, and demodulation.
A key to the practicality of chaining techniques is
the extent to which so-called variable chainings can be restricted.
Syntactic ordering restrictions on terms
and the rewrite techniques which account for their completeness
considerably restrict variable chaining.
We show that variable elimination
is an admissible simplification techniques
within our redundancy framework,
and that consequently for dense total orderings without endpoints
no variable chaining is needed at all.
