Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
DOI10.1007/978-3-642-54624-2_5zbMATH Open1407.68312OpenAlexW8691849MaRDI QIDQ5403069FDOQ5403069
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
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
confluenceterminationalgebraic specificationssufficient completenessconditional term rewriting systemsincremental proofs
Cites Work
- Title not available (Why is that?)
- Operational termination of conditional term rewriting systems
- Sufficient completeness verification for conditional and constrained TRS
- Sufficient-completeness, ground-reducibility and their complexity
- Refutational theorem proving using term-rewriting systems
- Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications
- Principles of proof scores in CafeOBJ
- Proof scores in the OTS/CafeOBJ method.
- Modular and incremental automated termination proofs
- Modular and incremental proofs of AC-termination
- Title not available (Why is that?)
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
Uses Software
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)
