Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Conference Paper

Ordered Chaining for Total Orderings


Bachmair,  Leo
Programming Logics, MPI for Informatics, Max Planck Society;


Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

(Publisher version)

Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Bachmair, L., & Ganzinger, H. (1994). Ordered Chaining for Total Orderings. In A. Bundy (Ed.), Proceedings of the 12th International Conference on Automated Deduction (CADE-12) (pp. 435-450). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-AD92-2
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.