Combination of Compatible Reduction Orderings that are Total on Ground Terms
Aus International Center for Computational Logic
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
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},
}
