Constructor-Based Inductive Theorem Prover

DOI10.1007/978-3-642-40206-7_26MaRDI QIDQ2848959zbMATH OpenOpenAlexFDO

Authors Daniel Găină, Min Zhang, Yuki Chiba, 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)

Recommendations

• Proofs by induction in equational theories with constructors
• scientific article; zbMATH DE number 3891336
• scientific article; zbMATH DE number 3965464
• Constructor-based logics
• scientific article; zbMATH DE number 549978
• Building Theorem Provers
• Proving ground confluence and inductive validity in constructor based equational specifications
• Automatic proofs by induction in theories without constructors
• Focused Inductive Theorem Proving

Cited in

(10)

• Stability of termination and sufficient-completeness under pushouts via amalgamation
• Omitting types theorem in hybrid dynamic first-order logic with rigid symbols
• scientific article; zbMATH DE number 3870639 (Why is no real title available?)
• CITP
• Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool
• TIP: tools for inductive provers
• On Automation of OTS/CafeOBJ Method
• From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
• A Maude environment for CafeOBJ
• Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs

Describes a project that uses

Uses Software

• CIRC

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

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