- Titel
- Combination of Compatible Reduction Orderings that are Total on Ground Terms
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-788051
- Schriftenreihe
- LTCS-Report
- Bandnummer
- 96-05
- Erstveröffentlichung
- 1996
- DOI
- https://doi.org/10.25368/2022.68
- Abstract (EN)
- Reduction orderings that are compatible with an equational theory E and total on (the E-equivalence classes of) ground terms play an important rôle in automated deduction. We present a general approach for combining such orderings. To be more precise, we show how E1-compatible reduction orderings total on Σ1-ground terms and E2-compatible reduction orderings total on Σ2-ground terms can be used to construct an (E1[E2)-compatible reduction ordering total on (Σ1 [Σ2)-ground terms, provided that the signatures are disjoint and some other (rather weak) restrictions are satised. 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.
- Freie Schlagwörter (DE)
- Kürzungsanordnungen, automatische Abzüge, Grundbegriffe
- Freie Schlagwörter (EN)
- Reduction orderings, automated deduction, ground terms
- Klassifikation (DDC)
- 004
- Klassifikation (RVK)
- ST 136
- Publizierende Institution
- Aachen University of Technology, Aachen
- Version / Begutachtungsstatus
- angenommene Version / Postprint / Autorenversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-788051
- Veröffentlichungsdatum Qucosa
- 18.05.2022
- Dokumenttyp
- Bericht
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0