For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Syntactic Unification Problems under Constrained Substitutions
Kazuhiro TAKADA Yuichi KAJI Tadao KASAMI
IEICE TRANSACTIONS on Information and Systems
Publication Date: 1997/05/25
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Automata,Languages and Theory of Computing
unification problem, decidability, computational complexity, order-sorted signature, tree automata,
Full Text: PDF>>
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.