Combination of Compatible Reduction Orderings that are Total on Ground Terms

PublikationenPublications

• Nach AutorBy Author
  • Franz BaaderFranz Baader
• Nach ForschungsgruppeBy Research Group
  • AutomatentheorieAutomata Theory

Toggle side column

Combination of Compatible Reduction Orderings that are Total on Ground Terms

Franz BaaderFranz Baader

Datei:Baader-LTCS-96.ps.gz

• Download

Franz Baader
Combination of Compatible Reduction Orderings that are Total on Ground Terms
Technical Report, LuFg Theoretical Computer Science, RWTH Aachen, Germany, volume LTCS-96-05, 1996. LTCS-Report

• 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. We present a general approach for combining such orderings. To be more precise, we show how $E_1$-compatible reduction orderings total on $Sigma_1$-ground terms and $E_2$-compatible reduction orderings total on $Sigma_2$-ground terms can be used to construct an $(E_1cup E_2)$-compatible reduction ordering total on $(Sigma_1cup Sigma_2)$-ground terms, provided that the signatures 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

@techreport{ Baader-LTCS-96,
  author = {F. {Baader}},
  institution = {LuFg Theoretical Computer Science, RWTH Aachen, Germany},
  number = {LTCS-96-05},
  title = {Combination of Compatible Reduction Orderings that are Total on Ground Terms},
  type = {LTCS-Report},
  year = {1996},
}