Name
Abstract | ||
|---|---|---|
. We design new inference systems for total orderings by applyingrewrite techniques to chaining calculi. Equality relations may eitherbe specified axiomatically or built into the deductive calculus viaparamodulation or superposition. We demonstrate that our inference systemsare compatible with a concept of (global) redundancy for clausesand inferences that covers such widely used simplification techniques astautology deletion, subsumption, and demodulation. A key to the practicalityof... |
Year | DOI | Venue |
|---|---|---|
1994 | 10.1007/3-540-58156-1_32 | CADE |
Keywords | Field | DocType |
total orderings,ordered chaining,total order | Variable elimination,Chaining,Tautology (logic),Inference,Computer science,Algorithm,Redundancy (engineering),Rule of inference,Completeness (statistics),Syntax | Conference |
ISBN | Citations | PageRank |
3-540-58156-1 | 13 | 0.73 |
References | Authors | |
15 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Leo Bachmair | 1 | 1006 | 90.72 |
| Harald Ganzinger | 2 | 1513 | 155.21 |