Semantic confluence tests and completion methods
From MaRDI portal
Publication:3732980
DOI10.1016/S0019-9958(85)80005-XzbMath0598.68058OpenAlexW2022060249WikidataQ29398513 ScholiaQ29398513MaRDI QIDQ3732980
Publication date: 1985
Published in: Information and Control (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0019-9958(85)80005-x
Abstract data types; algebraic specification (68Q65) Mechanization of proofs and logical operations (03B35) Equational logic, Mal'tsev conditions (08B05) Equational classes, universal algebra in model theory (03C05)
Related Items
Bottom-up tree pushdown automata: Classification and connection with rewrite systems, On sufficient-completeness and related properties of term rewriting systems, Inductive theorem proving by consistency for first-order clauses, Computing linearizations using test sets, A proof system for conditional algebraic specifications, Proof by consistency in conditional equational theories, Completion procedures as semidecision procedures, Proving ground confluence and inductive validity in constructor based equational specifications, Ground reducibility is EXPTIME-complete, Computing ground reducibility and inductively complete positions, Inductive proofs by specification transformations, Proofs in parameterized specifications, Bottom-up tree pushdown automata and rewrite systems, On relationship between term rewriting systems and regular tree languages, Open problems in rewriting, Encompassment properties and automata with constraints, Towards an efficient construction of test sets for deciding ground reducibility, Termination of constructor systems, The first-order theory of one-step rewriting is undecidable, Sufficient-completeness, ground-reducibility and their complexity, Reasoning with conditional axioms, Abstract data type systems, On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, Test sets for the universal and existential closure of regular tree languages., On ground-confluence of term rewriting systems, A rationale for conditional equational programming, Pumping, cleaning and symbolic constraints solving, Towards a foundation of completion procedures as semidecision procedures, Undecidability of ground reducibility for word rewriting systems with variables, Narrowing based procedures for equational disunification, Testing for the ground (co-)reducibility property in term-rewriting systems, Decidability of regularity and related properties of ground normal form languages, Proving weak properties of rewriting, Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness, On the connection between narrowing and proof by consistency, Automating inductionless induction using test sets, The first-order theory of linear one-step rewriting is undecidable, 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, Deductive and inductive synthesis of equational programs
