Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications

DOI10.1007/978-3-642-54624-2_5zbMath1407.68312OpenAlexW8691849MaRDI QIDQ5403069

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

algebraic specificationsconfluenceterminationsufficient completenessconditional term rewriting systemsincremental proofs

Mathematics Subject Classification ID

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

Related Items (3)

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

Uses Software

• OBJ3

Cites Work

• Unnamed Item
• Unnamed Item
• Sufficient completeness verification for conditional and constrained TRS
• Refutational theorem proving using term-rewriting systems
• Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications
• Operational termination of conditional term rewriting systems
• Principles of proof scores in CafeOBJ
• Modular and incremental automated termination proofs
• Sufficient-completeness, ground-reducibility and their complexity
• Modular and incremental proofs of AC-termination
• Formal Methods for Open Object-Based Distributed Systems

This page was built for publication: Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications