naistar (NAIST Academic Repository) >
学術リポジトリ naistar / NAIST Academic Repository naistar >
テクニカルレポート / Technical Report >
Please use this identifier to cite or link to this item:
|Title: ||A sufficient condition for the termination of the procedure for solving an order-sorted unification problem|
|Authors: ||Takai, Toshinori|
|Issue Date: ||Aug-1999|
|Publisher: ||Nara Institute of Science and Technology|
|Series/Report no.: ||Information Science Technical Report ~ TR99010|
|Abstract: ||The authors have proposed a procedure for solving an order-sorted unification problem in an equational theory which is defined by a confluent TRS. The procedure requires an instance of the problem to satisfy that the TRS is right-linear and the goal terms are linear and share no variables. If a given instance of the problem satisfies these conditions and the procedure halts, then it answers correctly. In this paper, we propose a sufficient condition to terminate the procedure. The unification procedure constructs tree automata to solve the problem. The proposed condition guarantees the number of the states of the tree automata to be finite and provides a decidable subclass of the order-sorted unification problems.|
|Text Version: ||author|
|Appears in Collections:||テクニカルレポート / Technical Report|
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.