Principles of proof scores in CafeOBJ

DOI10.1016/J.TCS.2012.07.041MaRDI QIDQ1929233zbMATH OpenOpenAlexFDO

Authors 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

algebraic specificationsCafeOBJproof scoresterm rewritingtheorem proving

Mathematics Subject Classification ID

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

Recommendations

• Proof scores in the OTS/CafeOBJ method.
• Generic proof scores for generate \& check method in CafeOBJ
• On Automation of OTS/CafeOBJ Method
• scientific article; zbMATH DE number 2172803
• Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method

Cites work

• CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
• Constructor-based institutions
• Coverset induction with partiality and subsorts: a powerlist case study
• scientific article; zbMATH DE number 4130339 (Why is no real title available?)
• scientific article; zbMATH DE number 3970817 (Why is no real title available?)
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 1942449 (Why is no real title available?)
• scientific article; zbMATH DE number 3019695 (Why is no real title available?)
• Institution-independent model theory
• Institutions: abstract model theory for specification and programming
• Isabelle/HOL. A proof assistant for higher-order logic
• Logical foundations of CafeOBJ
• Logical systems for structured specifications.
• Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Proof scores in the OTS/CafeOBJ method.
• Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method
• Specifications in an arbitrary institution
• Structural induction in institutions
• Twenty years of rewriting logic

Cited in

(18)

• Logical foundations of CafeOBJ
• From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
• Stability of termination and sufficient-completeness under pushouts via amalgamation
• A toolkit for generating and displaying proof scores in the OTS/CafeOBJ method
• Using CafeOBJ to mechanise refactoring proofs and application
• Generic proof scores for generate \& check method in CafeOBJ
• Liveness properties in CafeOBJ -- a case study for meta-level specifications
• scientific article; zbMATH DE number 1962762 (Why is no real title available?)
• Manifest domains: analysis and description
• A Maude environment for CafeOBJ
• Generate \& check method for verifying transition systems in CafeOBJ
• 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
• Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method
• Proof scores in the OTS/CafeOBJ method.
• Relationship between FAC at plasma sheet boundary layers and AE index during storms from August to October, 2001

Describes a project that uses

Uses Software

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

This page was built for publication: Principles of proof scores in CafeOBJ

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