Combination of Compatible Reduction Orderings that are Total on Ground Terms

Franz BaaderFranz Baader

Franz Baader
Combination of Compatible Reduction Orderings that are Total on Ground Terms
In G. Winskel, eds., Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS-97), 2-13, 1997. IEEE Computer Society Press

Details
Bibtex

KurzfassungAbstract
Reduction orderings that are compatible with an equational theory E and total on (the E-equivalence classes of) ground terms play an important role in automated deduction. This paper presents a general approach for combining such orderings: it shows how E1-compatible reduction orderings total on S1-ground terms and E2-compatible reduction orderings total on S2-ground terms can be used to construct an E-compatible reduction ordering total on S-ground terms (where F is the union of the theories E1 and E2, and S is the union of the signatures S1 and S2), provided that S1 and S2 are disjoint and some other (rather weak) restrictions are satisfied. This work was motivated by the observation that it is often easier to construct such orderings for "small" signatures and theories separately, rather than directly for their union.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@inproceedings{ Baader-LICS-97,
  address = {Warsaw, Poland},
  author = {F. {Baader}},
  booktitle = {Proceedings of the Twelfth Annual {IEEE} Symposium on Logic in Computer Science (LICS-97)},
  editor = {G. {Winskel}},
  pages = {2--13},
  publisher = {IEEE Computer Society Press},
  title = {Combination of Compatible Reduction Orderings that are Total on Ground Terms},
  year = {1997},
}