Simultaneous checking of completeness and ground confluence for algebraic specifications

DOI10.1145/1507244.1507250MaRDI QIDQ2946578zbMATH OpenOpenAlexFDO

Authors Adel Bouhoula

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1507244.1507250

zbMATH Keywords

algebraic specificationsautomated deductioncompletenessground confluenceparameterizationterm rewriting systems

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Abstract data types; algebraic specification (68Q65)

Recommendations

• A proof system for conditional algebraic specifications
• An algorithm to recognize sufficient completeness of algebraic specification of an abstract data type
• Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
• scientific article; zbMATH DE number 3990847
• scientific article; zbMATH DE number 3913659

Cited in

(12)

• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• Constructive consistency checking for partial specification in Z
• Ground confluence of order-sorted conditional specifications modulo axioms
• scientific article; zbMATH DE number 7340317 (Why is no real title available?)
• Mechanically certifying formula-based Noetherian induction reasoning
• Improving rewriting induction approach for proving ground confluence
• Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
• Checking Sufficient Completeness by Inductive Theorem Proving
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
• A verified algorithm for deciding pattern completeness
• A nominal approach to equational problems in languages with binders
• A verified algorithm for deciding pattern completeness with optimal asymptotic complexity

This page was built for publication: Simultaneous checking of completeness and ground confluence for algebraic specifications

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