Principles of proof scores in CafeOBJ

DOI10.1016/j.tcs.2012.07.041zbMath1253.68220OpenAlexW2044923579MaRDI QIDQ1929233

Kokichi Futatsugi, Daniel Găină, Kazuhiro Ogata

Publication date: 7 January 2013

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

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

zbMATH Keywords

theorem provingalgebraic specificationsterm rewritingCafeOBJproof scores

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Grammars and rewriting systems (68Q42)

Related Items

Generic Proof Scores for Generate & Check Method in CafeOBJ, Liveness Properties in CafeOBJ – A Case Study for Meta-Level Specifications, From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories, Stability of termination and sufficient-completeness under pushouts via amalgamation, Incremental Proofs of Termination, Confluence and Sufficient Completeness of OBJ Specifications, On Automation of OTS/CafeOBJ Method, Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool, Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs, Manifest domains: analysis and description, A Maude environment for CafeOBJ, Generate & Check Method for Verifying Transition Systems in CafeOBJ

Uses Software

• ACL2
• Isabelle/HOL
• OBJ3
• CafeOBJ
• ITP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Structural induction in institutions
• Specifications in an arbitrary institution
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Isabelle/HOL. A proof assistant for higher-order logic
• Logical foundations of CafeOBJ
• Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
• Logical systems for structured specifications.
• Institution-independent model theory
• Constructor-Based Institutions
• Institutions: abstract model theory for specification and programming
• Twenty Years of Rewriting Logic
• Coverset Induction with Partiality and Subsorts: A Powerlist Case Study
• Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method
• Formal Methods for Open Object-Based Distributed Systems