MPI-I-93-250
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.
Note:
Short version in Proc.~CADE'94, LNAI 814, pp.\ 435--450, 1994
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1993-250
BibTeX
@TECHREPORT{BachmairGanzinger-93-mpii250,
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},
}