Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs

DOI10.1007/978-3-642-54624-2_31zbMATH Open1407.68298OpenAlexW2125379699MaRDI QIDQ5403086FDOQ5403086

Authors: 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_31

Recommendations

• Rewriting Techniques and Applications
• The term rewriting approach to automated theorem proving
• scientific article; zbMATH DE number 4053062
• scientific article; zbMATH DE number 4074535
• Refutational theorem proving using term-rewriting systems
• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
• Publication:3490953
• scientific article; zbMATH DE number 2016837

zbMATH Keywords

searchtheorem provingproof score(bounded) model checkingrewrite theory specification

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Title not available (Why is that?)
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Title not available (Why is that?)
• Constructor-Based Inductive Theorem Prover
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• Using encryption for authentication in large networks of computers
• A hidden agenda
• CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
• Circular coinduction: a proof theoretical foundation
• Title not available (Why is that?)
• Abstract logical model checking of infinite-state systems using narrowing
• On the security of public key protocols
• An attack on the Needham-Schroeder public-key authentication protocol
• Equational abstractions
• Principles of proof scores in CafeOBJ
• Constructor-based logics
• Proof scores in the OTS/CafeOBJ method.
• Title not available (Why is that?)
• Modeling and verification of real-time systems based on equations
• Title not available (Why is that?)
• Proving Safety Properties of Rewrite Theories
• Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method
• Title not available (Why is that?)

Cited In (2)

• Proof scores in the OTS/CafeOBJ method.
• A Maude environment for CafeOBJ

Uses Software

• TRAM
• OBJ3
• CIRC
• CafeOBJ
• Maude
• UNITY
• CITP

This page was built for publication: Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs

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