Jouannaud, Jean-Pierre 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). Page: −5 −4 −3 −2 −1 ±0 +1 +2 +3 +4 +5 Show Scanned Page Cited in 6 Documents 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 Keywords:term rewriting; equational deduction; Church-Rosser property; confluence; coherence; critical pairs; data types; algebraic specifications; consistency Citations:Zbl 0516.00024 PDFBibTeX XML