Semantic confluence tests and completion methods

DOI10.1016/S0019-9958(85)80005-XMaRDI QIDQ3732980zbMATH OpenOpenAlexDBLPWikidataFDO

Authors David A. Plaisted

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

zbMATH Keywords

completionequational logicterm rewriting system

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05) Equational logic, Mal'tsev conditions (08B05) Abstract data types; algebraic specification (68Q65)

Recommendations

• Ordered rewriting and confluence
• A reduction-preserving completion for proving confluence of non-terminating term rewriting systems
• A reduction-preserving completion for proving confluence of non-terminating term rewriting systems
• Confluence of non-left-linear TRSs via relative termination
• Testing confluence of nonterminating rewriting systems

Cited in

(44)

• 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
• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• Sufficient-completeness, ground-reducibility and their complexity
• Pumping, cleaning and symbolic constraints solving
• Proving ground confluence and inductive validity in constructor based equational specifications
• 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
• Triangulation in rewriting
• On the connection between narrowing and proof by consistency
• Proving weak properties of rewriting
• Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
• Inductive theorem proving by consistency for first-order clauses
• Decidability of regularity and related properties of ground normal form languages
• Computing linearizations using test sets
• A proof system for conditional algebraic specifications
• Proof by consistency in conditional equational theories
• Completion procedures as semidecision procedures
• Towards a foundation of completion procedures as semidecision procedures
• Late and early semantics coincide for testing
• Undecidability of ground reducibility for word rewriting systems with variables
• Testing for the ground (co-)reducibility property in term-rewriting systems
• Tail reduction free term rewriting systems revisited
• Automating inductionless induction using test sets
• On ground-confluence of term rewriting systems
• A rationale for conditional equational programming

This page was built for publication: Semantic confluence tests and completion methods

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3732980)