DocumentCode :
2838828
Title :
On the termination of an algorithm for unification in equational theories
Author :
Aguzzi, Gianni ; Verri, M. Cecilia
Author_Institution :
Dipartimento di Sistemi e Inf., Firenze Univ., Italy
fYear :
1989
fDate :
22-24 Nov 1989
Firstpage :
1034
Lastpage :
1039
Abstract :
The termination properties of a semantic unification procedure for the problem t=Rt´ are studied, where R is expressed by means of a canonical term rewriting system and t´ is a round term not containing any defined function symbol. The procedure is shown to be terminating whenever R satisfies a condition whose main point is the `strictly conicity´ of the recursive right hand side of the rules. Moreover, the necessity of such a condition is shown for a suitable class of term rewriting systems and equations
Keywords :
logic programming; rewriting systems; canonical term rewriting system; equational theories; semantic unification procedure; strictly conicity; term rewriting systems; termination properties; Equations; Logic; Sufficient conditions;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
TENCON '89. Fourth IEEE Region 10 International Conference
Conference_Location :
Bombay
Type :
conf
DOI :
10.1109/TENCON.1989.177107
Filename :
177107
Link To Document :
بازگشت