Syntactic Unification Problems under Constrained Substitutions

Kazuhiro TAKADA  Yuichi KAJI  Tadao KASAMI  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E80-D   No.5   pp.553-561
Publication Date: 1997/05/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Automata,Languages and Theory of Computing
Keyword: 
unification problem,  decidability,  computational complexity,  order-sorted signature,  tree automata,  

Full Text: PDF>>
Buy this Article



Summary: 
Some kind of practical problems such as security verification of cryptographic protocols can be described as a problem to accomplish a given purpose by using limited operations and limited materials only. To model such problems in a natural way, unification problems under constrained substitutions have been proposed. This paper is a collection of results on the decidability and the computational complexity of a syntactic unification problem under constrained substitutions. A number of decidable, undecidable, tractable and intractable results of the problem are presented. Since a unification problem under constrained substitutions can be regarded as an order-sorted unification problem with term declarations such that the number of sorts is only one, the results presented in this paper also indicate how the intractability of order-sorted unification problems is reduced by restecting the number of sorts to one.