Result: The joinability and unification problems for confluent semi-constructor TRSs

Title:
The joinability and unification problems for confluent semi-constructor TRSs
Authors:
MITSUHASHI, Ichiro, OYAMAGUCHI, Michio, OHTA, Yoshikatsu, YAMADA, Toshiyuki
Source:
RTA 2004 : rewriting techniques and applications (Aachen, 3-5 June 2004)Lecture notes in computer science. :285-300
Publisher Information:
Berlin: Springer, 2004.
Publication Year:
2004
Physical Description:
print, 15 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie programmation, Programming theory, Décidabilité, Decidability, Decidibilidad, Système réécriture, Rewriting systems, Unification, Unificación
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Faculty of Engineering, Mie University, 1515 Kamihama-cho, Tsu-shi, 514-8507, Japan
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=15851917
Rights:
Copyright 2004 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.15851917
Database:
PASCAL Archive

Further Information

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.