EQUATIONAL COMPLETION IN ORDER-SORTED ALGEBRAS

被引:9
作者
GNAEDIG, I
KIRCHNER, C
KIRCHNER, H
机构
[1] LORIA,F-54506 VANDOEUVRE NANCY,FRANCE
[2] CTR RECH INFORMAT NANCY,F-54506 VANDOEUVRE NANCY,FRANCE
关键词
D O I
10.1016/0304-3975(90)90034-F
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We describe and prove completion procedures for equational term rewriting systems in order-sorted algebras, using the technique of proof orderings. Problems specific to order-sorted equational logic are emphasized. © 1990.
引用
收藏
页码:169 / 202
页数:34
相关论文
共 62 条
[1]  
Bachmair L., 1986, Proceedings of the Symposium on Logic in Computer Science (Cat. No.86CH2321-8), P346
[2]  
BACHMAIR L, 1988, THESIS U ILLINOIS UR
[3]  
BACHMAIR L, 1987, 2ND P C REWR TECHN A
[4]  
BURSTALL RM, 1980, 1980 C REC LISP C, P136
[5]  
CUNNINGHAM RJ, 1983, REWRITE SYSTEMS LATT
[6]   ORDERINGS FOR TERM-REWRITING SYSTEMS [J].
DERSHOWITZ, N .
THEORETICAL COMPUTER SCIENCE, 1982, 17 (03) :279-301
[7]   TERMINATION OF REWRITING [J].
DERSHOWITZ, N .
JOURNAL OF SYMBOLIC COMPUTATION, 1987, 3 (1-2) :69-116
[8]   PROVING TERMINATION WITH MULTI-SET ORDERINGS [J].
DERSHOWITZ, N ;
MANNA, Z .
COMMUNICATIONS OF THE ACM, 1979, 22 (08) :465-476
[9]  
DERSHOWITZ N, 1988, MACH INTELL, V11, P21
[10]  
DICK AJJ, 1985, P EUROCA C