NAISTAR
Advanced Search
Japanese | English

naistar (NAIST Academic Repository) >
学術リポジトリ naistar / NAIST Academic Repository naistar >
テクニカルレポート / Technical Report >

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=100019038&oldid=24235
Fulltext: http://library.naist.jp/mylimedio/dllimedio/show.cgi?bookid=100019038&oldid=24235
ISSN: 0919-9527
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.

 

Copyright (c) 2007-2012 Nara Institute of Science and Technology All Rights Reserved.
DSpace Software Copyright © 2002-2010  Duraspace - Feedback