MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


Ordered chaining for total orderings

Bachmair, Leo and Ganzinger, Harald

December 1993, 20 pages.

Status: available - back from printing

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.
Short version in Proc.~CADE'94, LNAI 814, pp.\ 435--450, 1994

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Bachmair, Leo and Ganzinger, Harald},
  TITLE = {Ordered chaining for total orderings},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-250},
  MONTH = {December},
  YEAR = {1993},
  ISSN = {0946-011X},
  NOTE = {Short version in Proc.~CADE'94, LNAI 814, pp.\ 435--450, 1994},