Semantic confluence tests and completion methods
From MaRDI portal
Publication:3732980
DOI10.1016/S0019-9958(85)80005-XzbMath0598.68058WikidataQ29398513 ScholiaQ29398513MaRDI QIDQ3732980
Publication date: 1985
Published in: Information and Control (Search for Journal in Brave)
68Q65: Abstract data types; algebraic specification
03B35: Mechanization of proofs and logical operations
08B05: Equational logic, Mal'tsev conditions
03C05: Equational classes, universal algebra in model theory
Related Items
Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness, Towards a foundation of completion procedures as semidecision procedures, Undecidability of ground reducibility for word rewriting systems with variables, Testing for the ground (co-)reducibility property in term-rewriting systems, Automating inductionless induction using test sets, On ground-confluence of term rewriting systems, A rationale for conditional equational programming, On sufficient-completeness and related properties of term rewriting systems, Narrowing based procedures for equational disunification, The first-order theory of linear one-step rewriting is undecidable, Deductive and inductive synthesis of equational programs, Bottom-up tree pushdown automata: Classification and connection with rewrite systems, Abstract data type systems, Test sets for the universal and existential closure of regular tree languages., A strong restriction of the inductive completion procedure, Induction = I-axiomatization + first-order consistency., The undecidability of the first-order theories of one step rewriting in linear canonical systems, Ground reducibility is EXPTIME-complete, Reasoning with conditional axioms, Sufficient-completeness, ground-reducibility and their complexity
