Constructor-Based Inductive Theorem Prover

DOI10.1007/978-3-642-40206-7_26zbMath1396.68112OpenAlexW133357462MaRDI QIDQ2848959

Yuki Chiba, Min Zhang, Daniel Găină, Yasuhito Arimoto

Publication date: 13 September 2013

Published in: Algebra and Coalgebra in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-40206-7_26

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (8)

From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories ⋮ Stability of termination and sufficient-completeness under pushouts via amalgamation ⋮ 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 ⋮ A Maude environment for CafeOBJ ⋮ CITP ⋮ Omitting types theorem in hybrid dynamic first-order logic with rigid symbols

Uses Software

• CIRC

This page was built for publication: Constructor-Based Inductive Theorem Prover