×

Confluent and coherent equational term rewriting systems application to proofs in abstract data types. (English) Zbl 0522.68013

Trees in algebra and programming, CAAP ’83, Proc. 8th Colloq., L’Aquila/Italy 1983, Lect. Notes Comput. Sci. 159, 269-283 (1983).

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68W30 Symbolic computation and algebraic computation
68P05 Data structures
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
08A50 Word problems (aspects of algebraic structures)
03F05 Cut-elimination and normal-form theorems

Citations:

Zbl 0516.00024