Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications

DOI10.1007/978-3-642-54624-2_5MaRDI QIDQ5403069zbMATH OpenOpenAlexFDO

Authors Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi

Publication date 25 March 2014

Published in Specification, Algebra, and Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-54624-2_5

zbMATH Keywords

confluenceterminationalgebraic specificationssufficient completenessconditional term rewriting systemsincremental proofs

Mathematics Subject Classification ID

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

Recommendations

• Soundness in verification of algebraic specifications with OBJ
• Simultaneous checking of completeness and ground confluence for algebraic specifications
• A proof system for conditional algebraic specifications
• On Equality Predicates in Algebraic Specification Languages
• CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification

Cites work

• scientific article; zbMATH DE number 1729952 (Why is no real title available?)
• scientific article; zbMATH DE number 4164121 (Why is no real title available?)
• Modular and incremental automated termination proofs
• Modular and incremental proofs of AC-termination
• Operational termination of conditional term rewriting systems
• Principles of proof scores in CafeOBJ
• Proof scores in the OTS/CafeOBJ method.
• Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications
• Refutational theorem proving using term-rewriting systems
• Sufficient completeness verification for conditional and constrained TRS
• Sufficient-completeness, ground-reducibility and their complexity

Cited in

(8)

• Stability of termination and sufficient-completeness under pushouts via amalgamation
• Ground confluence of order-sorted conditional specifications modulo axioms
• Generate \& check method for verifying transition systems in CafeOBJ
• Soundness in verification of algebraic specifications with OBJ
• Simultaneous checking of completeness and ground confluence for algebraic specifications
• On Equality Predicates in Algebraic Specification Languages
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
• Checking Sufficient Completeness by Inductive Theorem Proving

Describes a project that uses

Uses Software

• OBJ3

This page was built for publication: Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications

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