Stability of termination and sufficient-completeness under pushouts via amalgamation

DOI10.1016/j.tcs.2020.09.024zbMath1464.68215OpenAlexW3084627350MaRDI QIDQ2215962

Kazuhiro Ogata, Kokichi Futatsugi, Daniel Găină, Masaki Nakamura

Publication date: 15 December 2020

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2020.09.024

zbMATH Keywords

reducibilityalgebraic specificationterm rewritingpushoutsufficient-completenessparameterized specification

Mathematics Subject Classification ID

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

Uses Software

• CafeOBJ
• Maude
• CITP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Parametrization for order-sorted algebraic specification
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Operational termination of conditional term rewriting systems
• On sufficient-completeness and related properties of term rewriting systems
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Birkhoff style calculi for hybrid logics
• Observational logic, constructor-based logic, and their duality.
• Principles of proof scores in CafeOBJ
• Interpolation in logics with constructors
• Foundations of logic programming in hybrid logics with user-defined sharing
• Constructor-based observational logic
• Institution-independent model theory
• Modular and incremental automated termination proofs
• Sufficient-completeness, ground-reducibility and their complexity
• Modular and incremental proofs of AC-termination
• Constructor-Based Inductive Theorem Prover
• Combinatorics of $\lambda$-terms: a natural approach
• Order-Sorted Parameterization and Induction
• Institutions: abstract model theory for specification and programming
• Forcing and Calculi for Hybrid Logics
• Initial semantics in logics with constructors
• Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications

This page was built for publication: Stability of termination and sufficient-completeness under pushouts via amalgamation