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
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
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.pdf - 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|