A sufficient condition for the termination of the procedure for solving an order-sorted unification problem


NAIST \| Library	Advanced Search	Japanese \| English

Please use this identifier to cite or link to this item: http://hdl.handle.net/10061/3132

Title:	A sufficient condition for the termination of the procedure for solving an order-sorted unification problem
Authors:	Takai, Toshinori Kaji, Yuichi Seki, Hiroyuki タカイ, トシノリカジ, ユウイチセキ, ヒロユキ高井, 利憲楫, 勇一関, 浩之
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.
URI:	http://hdl.handle.net/10061/3132
URI:	http://library.naist.jp/mylimedio/dllimedio/show.cgi?bookid=24235
Fulltext:	http://library.naist.jp/mylimedio/dllimedio/show.cgi?bookid=24235
ISSN:	0919-9527
Text Version:	author
Appears in Collections:	テクニカルレポート / Technical Report

Files in This Item:

There are no files associated with this item.