Combination of Compatible Reduction Orderings that are Total on Ground Terms

From International Center for Computational Logic

Toggle side column

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
Proceedings of the 10th International Workshop on Unification, UNIF-96, CIS-Report 96-91, 97-106, 1996. CIS, Universität München
  • 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. It has turned out to be rather hard to define such orderings. This paper supports the process of designing compatible total reduction orderings. It describes how total reduction orderings $>_1$ and $>_2$ that are respectively compatible with $E_1$ and $E_2$ can be combined to a total reduction ordering $>$ that is compatible with $E_1 cup E_2$, provided that the theories are over disjoint signatures and some other properties are satisfied.
  • Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@inproceedings{ Baader-UNIF-96,
  author = {F. {Baader}},
  booktitle = {Proceedings of the 10th International Workshop on Unification, {UNIF-96}, CIS-Report 96-91},
  pages = {97--106},
  publisher = {CIS, Universit{\"a}t M{\"u}nchen},
  title = {Combination of Compatible Reduction Orderings that are Total on Ground Terms},
  year = {1996},
}