The Joinability and Unification Problems for Confluent Semi-constructor TRSs
| Autor: | Yoshikatsu Ohta, Ichiro Mitsuhashi, Michio Oyamaguchi, Toshiyuki Yamada |
|---|---|
| Rok vydání: | 2004 |
| Předmět: |
Discrete mathematics
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Unification Simple (abstract algebra) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Modulo ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION Tree automaton Rewriting Term (logic) Decidability Mathematics Variable (mathematics) |
| Zdroj: | Rewriting Techniques and Applications ISBN: 9783540221531 RTA |
| DOI: | 10.1007/978-3-540-25979-4_20 |
| Popis: | The unification problem for term rewriting systems (TRSs) is the problem of deciding, for a TRS R and two terms s and t, whether s and t are unifiable modulo R. Mitsuhashi et al. have shown that the problem is decidable for confluent simple TRSs. Here, a TRS is simple if the right-hand side of every rewrite rule is a ground term or a variable. In this paper, we extend this result and show that the unification problem for confluent semi-constructor TRSs is decidable. Here, a semi-constructor TRS is such a TRS that every subterm of the right-hand side of each rewrite rule is ground if its root is a defined symbol. We first show the decidability of joinability for confluent semi-constructor TRSs. Then, using the decision algorithm for joinability, we obtain a unification algorithm for confluent semi-constructor TRSs. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|