Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Ordered chaining for total orderings

Bachmair, Leo and Ganzinger, Harald

MPI-I-93-250. December 1993, 20 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-93-250.pdfMPI-I-93-250.pdfMPI-I-93-250.dvi - MPI-I-93-250.dvi
108 KBytes; 169 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
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},